Contract Verification
Feature: Z3 static contract verification Related metric: Safety (measures contract enforcement effectiveness) C# equivalent: None (C# Code Contracts was abandoned)
Overview
Calor uses Z3 to verify contract obligations inside an explicitly modeled subset. A result is always labeled with one of seven statuses, so a conditional or unavailable proof cannot be mistaken for a clean proof.
This is different from syntax-constrained generation: it analyzes semantic obligations. It does not establish whole-program correctness.
Why It Matters
Static contract verification can surface these bugs before execution when the relevant invariant is expressed and its forms are modeled:
- Division by zero - modeled obligations can prove a divisor nonzero or expose a counterexample
- Bounds violations - modeled index constraints can be proved or refuted
- Integer overflow - fixed-width arithmetic can be checked within the supported subset
- Null dereferences - modeled reference facts can establish non-null use
- Invalid state - modeled invariants can be proved or refuted
These bugs cannot be caught by grammar-constrained generation—syntax doesn't encode invariants.
How It's Measured
Contracts use the schema 2.0 seven-status vocabulary:
| Result | Meaning | Proof-based guard removal |
|---|---|---|
proven | The obligation holds under the modeled semantics | Eligible only when non-vacuous and assumption-free |
refuted | A violation exists | Not authorized; counterexample when available |
assumed | The proof depends on named assumptions | Not authorized |
unknown | Z3 could not decide | Not authorized |
timeout | Solver budget exhausted | Not authorized |
unsupported | Form or runtime semantics outside the model | Not authorized |
unavailable | No solver was available | Not authorized |
The metric tracks the distribution across these categories. Runtime checks
separately require supported lowering and an enabled contract mode.
--contract-mode off emits no contract guards; it does not disable checked
arithmetic. See
verification modes and limits.
This page describes current semantics, not a new measurement of historical benchmarks. Their recorded versions and results remain unchanged; see snapshot provenance and limits.
Example
The repository includes a deliberately refutable postcondition fixture:
§M{m1:OutcomeRefuted}
§F{f1:Dec:pub} (i32:x) -> i32
§Q (> x 0)
§S (> result 10)
§R (- x 1)
When compiled with --verify, Z3 binds result to the body expression and
checks whether the postcondition can fail:
calor -i math.calr -o math.g.cs --verify
The fixture produces Calor0712 (PostconditionMayBeViolated) with status
refuted. Its regression test requires a non-empty structured counterexample
with a result binding. The renderer begins that model with Counterexample:;
the exact bindings and formatting are solver-dependent.
This is an implementation-postcondition check. It should not be read as a claim that verification proves arbitrary preconditions at every call site.
Verification Categories
What Z3 Catches
| Bug Category | Contract | Detection |
|---|---|---|
| Division by zero | §Q (!= divisor 0) | proven/refuted when modeled; otherwise a non-proven status |
| Negative index | §Q (>= index 0) | proven/refuted when modeled; otherwise a non-proven status |
| Out of bounds | §Q (< index len) | Array facts are conservatively assumed where models diverge |
| Invalid range | §S (>= result 0) | Postcondition receives one of the seven statuses |
| Integer overflow | Bounds on operands | Checked arithmetic may throw; a postcondition alone does not establish exception-free execution |
Postcondition Verification
A postcondition constrains normal returns, not whether every input returns successfully:
§F{f001:Square:pub} (i32:x) -> i32
§E{}
§Q (>= x 0)
§S (>= result 0)
§R (* x x)
For native Calor, x = 46340 returns 2147395600. x = 46341 instead throws
OverflowException during checked multiplication, before any normal return or
postcondition check. It does not return a wrapped negative value.
An additional upper bound of 46340 prevents this multiplication overflow.
The exception still occurs with --contract-mode off, and requesting
--verify does not make the call succeed. Imported C# modules can have a
different overflow policy; see integer overflow policy.
Supported Constructs
Z3 verification supports:
| Calor | Z3 | Description |
|---|---|---|
(+ a b) | a + b | Addition |
(- a b) | a - b | Subtraction |
(* a b) | a * b | Multiplication |
(/ a b) | a div b | Division |
(% a b) | a mod b | Modulo |
(== a b) | a = b | Equality |
(!= a b) | a ≠ b | Inequality |
(< a b) | a < b | Less than |
(<= a b) | a ≤ b | Less or equal |
(> a b) | a > b | Greater than |
(>= a b) | a ≥ b | Greater or equal |
(&& p q) | p ∧ q | Logical and |
(|| p q) | p ∨ q | Logical or |
(! p) | ¬p | Logical not |
Integers use fixed-width bit-vectors, supported C# promotion rules, and the module's overflow policy. A bit-vector encoding does not mean native arithmetic wraps at runtime. Selected boolean, string, array, quantifier, implication, and registered user-field forms are also modeled.
In v0.12, string-, array-, and user-type-carried proofs are demoted to
assumed where the Z3 and .NET null/length models diverge. Function calls in
contracts, floating point, computed array bases, and forms outside the positive
whitelist report unsupported.
Comparison with Runtime-Only
| Aspect | Runtime Only | Static + Runtime |
|---|---|---|
| When bugs found | At runtime | At compile time |
| Verification cost | None | Compile time (cached) |
| Runtime overhead | Enabled, supported checks | Eligible clean proven guards may be removed |
| Coverage | Supported runtime lowering | Supported runtime lowering and modeled proof constructs |
Static verification complements runtime checking; it does not replace it.
Non-proven statuses never authorize proof-based removal. Structured early and
nested returns are supported. Opaque raw-C# bodies with postconditions are
rejected with Calor1001; iterator postconditions are rejected with Calor1004.
Why C# Cannot Do This
C# Code Contracts (2008-2015) attempted similar verification but was abandoned:
- Static analyzer was slow and unreliable
- Developers didn't write contracts consistently
- No integration with the language syntax
Calor makes contracts first-class syntax, which lets agents generate and inspect them as part of normal source authoring. They still require review: a solver can only verify the obligation that was written and modeled.
Configuration
# Enable verification (recommended)
calor -i app.calr -o app.g.cs --verify
# Custom timeout (default: 5 seconds per contract)
calor -i app.calr -o app.g.cs --verify --verification-timeout 10000
# Skip caching (for debugging)
calor -i app.calr -o app.g.cs --verify --no-cache
Next
- Effect Soundness - Verifying declared effects match actual behavior
- Verification Guarantees - Soundness boundaries and runtime-check rules