Static Contract Verification

Calor uses Z3 to verify contracts inside an explicitly modeled subset. The result is one of seven statuses. In released v0.12.1, --verify automatically removes an eligible runtime guard only for a clean, non-vacuous, assumption-free proven result. Every other result keeps its guard.

Overview

When you write contracts in Calor:

§F{f001:Square:pub} (i32:x) -> i32
  §Q (>= x 0)
  §S (>= result 0)
  §R (* x x)

For this integer-only signature, the compiler can prove that the postcondition holds under the precondition and encoded body. That is a proof of this obligation under Calor's modeled semantics—not a proof that the whole program is correct.

Enabling Static Verification

Use the --verify flag when compiling:

calor -i MyModule.calr -o MyModule.g.cs --verify

In v0.12.1 this also enables automatic removal of eligible proven guards.

Seven Verification Outcomes

Vacuous proofs carry a separate flag and keep their runtime checks. Preconditions are never elided on a satisfiability result.

Modeled Surface

Z3 verification supports:

Integer arithmetic is modeled with fixed-width bit-vectors and C#-compatible promotion rules where supported—not arbitrary-precision integers. Boolean, integer, selected string, array, quantifier, implication, and registered user-field forms are modeled with the restrictions below.

Function calls in contracts, floating-point contracts, unregistered fields, computed array bases, and forms outside the positive whitelist report unsupported.

How It Works

The verification process for postconditions:

1. Declare all parameters as symbolic Z3 variables
2. Assume all preconditions hold
3. Assert the negation of the postcondition
4. Check satisfiability:
   • UNSAT: No counterexample exists → Proven
   • SAT: Found counterexample → refuted
   • UNKNOWN: Timeout or too complex → timeout or unknown

For supported expressions, this proves the specific postcondition obligation under the encoded preconditions and modeled semantics. It does not prove the whole program correct.

Timeouts

The default solver budget is 5 seconds per contract. Use --timeout with calor verify, or --verification-timeout on the compile command.

Limitations

Function Calls

Contracts referencing other functions cannot be verified:

§S (> (strlen s) 0)  ; Unsupported - function call

Floating Point

Floating-point contracts report unsupported.

Strings and Nullable References

In v0.12, any proof that touches Z3's string sort is demoted to assumed. Z3 strings are null-free and byte-counted while .NET strings are nullable references whose length counts UTF-16 units. Array- and user-type-carried proofs are also assumed because Z3's sorts are total while .NET references may be null.

Non-ordinal string comparison modes are refused. Bare StartsWith, EndsWith, and IndexOf are also refused because .NET uses current-culture semantics for those overloads; state StringComparison.Ordinal explicitly.

Exceptional Arithmetic

Division and remainder carry divisor and signed-overflow side conditions. A proof that needs those conditions is assumed; conditional evaluation shapes that cannot preserve them are unsupported. Narrow arithmetic and signed/ unsigned combinations that do not match C# promotion are refused rather than guessed.

Runtime Lowering

Bodies with early, nested, or raw-C# returns can trigger Calor1001. In that case the compiler leaves the body untransformed and warns that postcondition runtime checks were not emitted. Static verification is separate from that lowering limitation.

Best Practices

Keep Contracts Simple

Simple arithmetic and comparison contracts verify quickly:

§Q (>= x 0)
§S (>= result 0)

Separate Concerns

Split complex contracts into multiple simpler ones:

; Instead of:
§S (and (>= result 0) (< result 100))

; Use:
§S (>= result 0)
§S (< result 100)

Treat Every Non-Proven Status as Information

assumed, unknown, timeout, unsupported, and unavailable mean different things and have different remedies. None means the code is wrong, and none is allowed to remove a runtime check.

Comparison with Runtime-Only Enforcement

Static verification complements runtime checking—it does not replace it. See Verification Guarantees for the v0.12 boundary and calor verify for the command contract.

What Calor Is Not

Calor is not a proof assistant like LEAN, Isabelle, or Rocq. The distinction matters:

No Proofs Required

In LEAN, proving a function returns a positive number requires explicit proof:

theorem sqrt_positive (x : ℝ) (h : x ≥ 0) : √x ≥ 0 := by
  exact Real.sqrt_nonneg x

In Calor, you declare the contract and Z3 attempts verification automatically. This floating-point example reports unsupported, which is an honest result:

§F{f001:Sqrt}(x: f64) -> f64
  §Q (>= x 0.0)
  §S (>= result 0.0)
  §R (* x x)

If Z3 cannot prove it, the runtime check remains where the emitter can lower it. Always treat Calor1001 as a loud exception to that runtime-check guarantee.

Lightweight by Design

Calor's verification is deliberately bounded:

• 5-second timeout per contract (configurable via --verification-timeout on compile or --timeout on calor verify)
• A positive modeled-forms whitelist rather than arbitrary math
• Graceful degradation to runtime checks

This is a feature, not a limitation. Verification never blocks your build indefinitely, and you don't need expertise in formal methods to benefit from it.

Z3 Installation

Z3 is bundled with the Calor compiler via the Microsoft.Z3 NuGet package. No separate installation is required.

If Z3 native libraries are missing on your platform, the compiler will:

1. Report unavailable
2. Skip the Z3 attempt
3. Continue compilation normally with all runtime checks

Verification Caching

Z3 verification results are automatically cached to disk. When you recompile a file with unchanged contracts, the compiler retrieves cached results instead of re-running Z3. This provides:

• Faster incremental builds: Unchanged contracts verify in milliseconds instead of seconds
• Reduced CI load: Build servers benefit from cached results across runs
• Deterministic cache keys: The same normalized obligation, settings, compiler semantics, and solver version reuse the same result

The cache includes contract and parameter shape, compiler and semantics versions, verification settings, and a format version. v0.12 bumped the format as proof semantics changed so older proven entries could not be reused.

To disable caching (e.g., for debugging), use --no-cache. To clear the cache, use --clear-cache.

Beyond Contracts: Refinement Types

Contracts verify behavior — preconditions and postconditions on function boundaries. Refinement types extend this to type-level constraints: instead of asserting (>= x 0) as a precondition, you declare the parameter as §I{i32:x} | (>= # INT:0) and the constraint becomes part of the type itself.

The obligation engine is an evolution of the assume-negate-check pattern described above:

1. Generation — The compiler creates verification obligations for every refined parameter and §PROOF statement
2. Solving — Each obligation goes through the same Z3 pipeline: assume preconditions, negate the condition, check satisfiability
3. Guard Discovery — For failed obligations, the engine discovers the simplest guard that would discharge them, validated by Z3
4. Policy — Configurable policies (default, strict, permissive) control whether failures are errors, warnings, or runtime guards

Where contracts are function-level assertions, refinement types are type-level constraints that feed the obligation engine. Refinement obligations are compile-time analysis only and do not emit runtime guards; review packets repeat that disclosure on every run that contains refinements.

• Refinement Types Reference
• Dependent Types Tutorial

See Also

• Contracts in Calor
• Compile Command
• Z3 Prover