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	Runtime Check
`proven`	The obligation holds under the modeled semantics	v0.12.1 removes an eligible guard only when non-vacuous and assumption-free
`refuted`	A violation exists	Preserved + counterexample when available
`assumed`	The proof depends on named assumptions	Preserved
`unknown`	Z3 could not decide	Preserved
`timeout`	Solver budget exhausted	Preserved
`unsupported`	Form or runtime semantics outside the model	Preserved
`unavailable`	No solver was available	Preserved

The metric tracks the distribution across these categories.

Example

The repository includes a deliberately refutable postcondition fixture:

Plain Text

§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:

Bash

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 v0.12.1 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	`§S (< result MAX_INT)`	Checked with fixed-width semantics in supported forms

Postcondition Verification

Z3 can prove that implementations satisfy their postconditions:

Plain Text

§F{f001:Square:pub} (i32:x) -> i32
  §E{}
  §Q (>= x 0)
  §S (>= result 0)         // Candidate for proof within the modeled subset
  §R (* x x)

Plain Text

// Example outcome: PROVEN, provided the proof is non-vacuous and assumption-free

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 and supported C# promotion rules. 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	Always	v0.12.1 removes eligible clean proven guards; all other guards remain
Coverage	All contracts	Supported constructs

Static verification complements runtime checking; it does not replace it. All non-proven statuses keep runtime checks. Calor1001 loudly reports the known early/nested-return lowering shape where a postcondition runtime check cannot currently be emitted.

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

Bash

# 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

Effect Soundness - Verifying declared effects match actual behavior
Verification Guarantees - Soundness boundaries and runtime-check rules