Static Contract Verification

Calor uses Z3 to verify contracts inside an explicitly modeled subset. The result is one of seven statuses. With optional --verify, the compiler removes an eligible runtime guard only for a clean, non-vacuous, assumption-free proven result. Other results never authorize proof-based removal. Runtime checks depend separately on contract mode and supported lowering; --contract-mode off emits no contract guards; it does not disable checked arithmetic. See verification modes and limits.

Overview

When you write contracts in Calor:

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

Native Calor checks this integer multiplication for overflow. x = 46340 returns 2147395600. x = 46341 satisfies the precondition, but multiplication throws OverflowException instead of returning a wrapped negative value. The postcondition constrains normal returns; it does not promise that every allowed input returns successfully.

Restricting x to 0..46340 avoids this multiplication overflow. --contract-mode off disables contract checks, not checked arithmetic. Optional --verify does not make this example return successfully for 46341. See integer overflow policy for the distinction between native Calor and imported C#.

Enabling Static Verification

Use the --verify flag when compiling:

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

This also enables removal of eligible proven guards. Add --keep-proven-guards to retain otherwise-emitted checks.

Seven Verification Outcomes

Vacuous proofs carry a separate flag and do not authorize guard removal. 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. Verification also follows the module's overflow policy; bit-vectors do not imply that native execution wraps on overflow. 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

Structured early and nested returns use a shared postcondition exit when checks are enabled. Opaque raw-C# bodies with postconditions are rejected with Calor1001; iterator postconditions are rejected with Calor1004. Static verification is separate from these runtime-lowering boundaries.

Runtime quantifiers also require a faithful finite domain and evaluation order. If those cannot be certified, Calor0326 fails compilation before guard elision; there is no silent static-only fallback. See the runtime quantifier limits.

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 current 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 request Z3 verification with --verify. 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)

An inconclusive proof does not authorize guard removal. Runtime checks still require an enabled contract mode and supported lowering; review Calor1001 and Calor1004 rather than treating these errors as successful enforcement.

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, relevant function-body context, module overflow policy, 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