Contracts and formal verification in Nova

Nova’s contract system lets you state what a function requires and ensures, then verifies those claims at compile time via an SMT solver. Nova uses enforce-with-elision (D24 / Plan 140), not debug-only asserts: a proven contract is elided (zero runtime cost, even in debug); an unproven one is enforced at runtime in both debug and release (fail-fast nova_contract_violation abort, never silent UB). You opt out of an unproven check only explicitly — per-fn #unchecked or build-policy --contracts=off. The opt-out has three scopes (Plan 140.3): #unchecked on a fn, #unchecked on a module (#unchecked before module X), or the build flag; and Eiffel-style per-kind granularity — #unchecked(requires) / #unchecked(ensures) / #unchecked(invariant) (combinable, fn or module) elide only the listed kinds. Without the SMT backend the proven set is empty, so every contract is checked (safe degrade, slower, not unsafe).

A contract violation — like an assert failure — is panic-class: caught by a consume/supervised scope it is classified as a Panic, not a recoverable Failure (Plan 140.3 / D13). A requires message may interpolate runtime values with ${...} — requires x > 0, "got ${x}" renders got -5 at the failing call (the message is built only on violation, never on the passing path; Plan 140.3).

Spec: D24 (SMT strategy) · D111 (assume / assert_static / #trusted) · D112 (bounded quantifiers) · D116 (Z3 backend).

Quickstart

// Simple precondition + postcondition.
#verify
fn withdraw(balance int, amount int) -> int
    requires amount > 0 && amount <= balance
    ensures  result == balance - amount
    ensures  result >= 0
{
    balance - amount
}

test "contracts quickstart: withdraw" {
    assert(withdraw(100, 30) == 70)
    assert(withdraw(50, 50)  == 0)
}

// REQUIRES_SMT_BACKEND z3

// Opaque helper + reveal in caller — Z3 proves the stronger contract.
#opaque #pure
fn double(x int) -> int
    requires x >= 0
    ensures  result >= 0
=> x * 2

#verify
fn caller_with_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2
{
    reveal double
    double(n)
}

test "contracts quickstart: opaque + reveal" {
    assert(double(5) == 10)
    assert(caller_with_reveal(7) == 14)
}

Contract clauses

Contract clauses appear between the parameter list and the { body (or => expression body). Multiple clauses of the same kind are allowed and are conjoined.

requires

A precondition. The SMT solver assumes it holds when verifying the body. Callers must satisfy it.

#verify
fn safe_div(a int, b int) -> int
    requires b != 0
    ensures  result * b == a - (a % b)
{
    a / b
}

Multiple requires clauses are equivalent to a single conjunction:

#verify
fn clamp(x int, lo int, hi int) -> int
    requires lo <= hi
    ensures  result >= lo && result <= hi
{
    if x < lo { lo } else if x > hi { hi } else { x }
}

Range conditions: use &&, never a chain

To constrain a value to a half-open range, write the canonical conjunction lo <= i && i < hi — not lo <= i < hi:

fn at(buf []int, i int) -> int
    requires 0 <= i && i < buf.len     // ✓ a real bounds check
=> buf[i]

A chained comparison such as 0 <= i < hi is a compile error (E_CMP_CHAIN_UNSUPPORTED) in Nova. It would otherwise parse as (0 <= i) < hi = bool < hi, which is vacuously true — silently turning the bounds contract into a no-op. Nova rejects the chain (and bool/unit operands of < <= > >=, E_RELATIONAL_OPERAND_NOT_ORDERED) at parse/check time; split into && as shown (Plan 150 / D248).

Self-access (@field, @len()) in method contracts

A method contract may refer to the receiver’s own state. Read a field with @field, or a built-in size accessor with @len() / @cap() / @byte_len() / @is_empty() (the call form is interchangeable with the field, @len() ≡ @len):

fn Vec[T] @index(i int) -> T
    requires 0 <= i && i < @len     // ✓ refers to the receiver's length
{
    unsafe { @data[i] }
}

The SMT solver models the receiver as an entity _self; each @field becomes an uninterpreted _field_<name>(_self), so @len in requires and @len in ensures denote the same term (consistent reasoning). Only reads are allowed — a contract is an expression, so there is no way to write a field in one.

When such a contract is unproven and fires at runtime, the violation message renders the self-access readably — requires failed: 0 <= i && i < @len — naming the actual field, not a placeholder (Plan 140.2 / D256 §Diagnostics).

Calling a non-accessor @method() (or a non-#pure / mut-receiver method) in a contract is a clear compile error — the SMT encoder cannot model arbitrary method bodies. Reference the field directly, or extract a #pure free function (Plan 140.2 / D256).

Bounds as an elidable contract (Vec @index)

Vec[T] @index/mut @index carry requires 0 <= i && i < @len, so an out-of-bounds v[i] is a contract violation. This makes bounds an elidable contract (D257), following the same enforce-with-elision model as any contract:

• a provably in-bounds access compiles with no runtime check (zero-cost);
• an unproven access keeps the check and aborts on OOB (in debug and release) — never silent UB.

The verifier proves an access in-bounds when the index is bounded by, e.g.:

for i in 0 .. v.len() {
    sum = sum + v[i]          // proven: i ∈ [0, v.len()) → check elided
    v[i] = v[i] * 2           // write-back also elided (in-place keeps length)
}
ro s = v[0 .. v.len()]        // slice v[a..b]: 0<=a && a<=b && b<=v.len() proven

fn at(v Vec[int], i int) -> int
    requires 0 <= i && i < v.len()
=> v[i]                       // cross-fn: bound comes from the `requires`

Elision needs the SMT backend (NOVA_SMT_BACKEND=z3); without it every access is checked (safe degrade). It also needs the vector’s length to be invariant in scope — a length-changing call (push/pop/…) on the same vector keeps the check (soundness). For accesses proven only via a requires, the check is kept under --contracts=off / #unchecked (where the requires is no longer enforced). @get/@first/@last return Option and stay None on OOB — they carry no bounds contract.

ensures and result

A postcondition. result refers to the return value of the function. Multiple ensures clauses are all independently checked.

#verify
fn abs_val(x int) -> int
    ensures result >= 0
    ensures result == x || result == -x
{
    if x >= 0 { x } else { -x }
}

old(...) in ensures

old(expr) captures the value of an expression at the function entry point, before the body runs. Useful for mutation contracts.

#verify
fn increment(mut n int) -> int
    ensures result == old(n) + 1
{
    n = n + 1
    n
}

decreases

Proves termination of recursive functions. The expression must strictly decrease on every recursive call. The SMT solver checks this as a well-foundedness obligation.

fn factorial(n int) -> int
    requires n >= 0
    decreases n
=> if n == 0 { 1 } else { n * factorial(n - 1) }

fn fib(n int) -> int
    requires n >= 0
    decreases n
=> if n < 2 { n } else { fib(n - 1) + fib(n - 2) }

Verification attributes

#verify

Strict SMT verification. The compiler encodes the function body and all contracts as an SMT query. If the solver cannot prove the contracts — unknown, timeout, or counterexample — compilation fails with an error (no runtime fallback).

Without #verify, contracts are still tried by the SMT solver, but a failure only produces a warning W2401/W2402 and a runtime check in debug — the build succeeds. #verify upgrades that to a hard error.

History: #verify was called #must_verify before Plan 33.3 Ф.9, when it was renamed. Any old text mentioning #must_verify on a function refers to #verify.

#verify
fn sum_nonneg(a int, b int) -> int
    requires a >= 0
    requires b >= 0
    ensures  result >= 0
{
    a + b
}

#pure

Marks a function as pure — no side effects, no effects in its row. Pure functions can be called freely inside contract expressions (requires/ensures/invariant), where effectful calls are forbidden.

#pure
fn is_positive(x int) -> bool => x > 0

#verify
fn safe_log(x int) -> int
    requires is_positive(x)    // #pure call allowed in contract
    ensures  result >= 0
{
    x - 1
}

#unverified

Opts out of SMT verification (not enforcement). The contracts are unproven, so they are enforced at runtime in both debug and release (enforce-with-elision — nothing is elided). Use for contracts the solver cannot handle (non-linear arithmetic, string predicates, etc.). To drop the runtime check too, use #unchecked / --contracts=off.

#unverified
fn safe_double(x int) -> int
    requires x > 0
    ensures  result == x * 2
=> x * 2

#must_verify (removed — use #verify)

#must_verify no longer exists. It was renamed to #verify in Plan 33.3 Ф.9. Writing #must_verify today is silently ignored by the parser (treated as an unknown attribute). Use #verify instead.

// Before Plan 33.3:  #must_verify fn f(...) ...
// After  Plan 33.3:  #verify      fn f(...) ...   ← use this
#verify
fn transfer_total(from_bal int, to_bal int, amount int) -> int
    requires amount > 0 && amount <= from_bal
    ensures  result == from_bal + to_bal
{
    (from_bal - amount) + (to_bal + amount)
}

#trusted

Used in two contexts:

1. with #trusted on a handler binding — skips axiom verification for that handler, accepts contracts as axioms on faith:

with #trusted Log = handler Log {
    Write(msg) { if msg > 0 { buf = msg } else { buf = 0 } }
    last() => buf
} { ... }

2. #trusted on a function containing assume — suppresses the trust-introduced warning:

#trusted
fn call_ffi() -> int {
    ro result = extern_fn()
    assume result >= 0    // documented FFI postcondition
    result
}

#pure function composition

#pure functions compose freely in contract expressions. This lets you build reusable predicates:

#pure
fn in_range(x int, lo int, hi int) -> bool => x >= lo && x <= hi

#verify
fn clamp_tight(x int) -> int
    ensures in_range(result, 0, 100)
{
    if x < 0 { 0 } else if x > 100 { 100 } else { x }
}

Non-pure functions in contracts are a compile error:

error: effectful function call in contract expression
  contracts require #pure or side-effect-free expressions

Proof helpers

assert_static

Inserts an intermediate proof step visible to the SMT solver. Breaks a complex contract into smaller, independently verifiable facts. Proven → elided (zero-cost, debug and release); unproven → runtime check kept in debug and release (enforce-with-elision).

#verify
fn transfer(from int, to int, amount int) -> int
    requires amount > 0 && amount <= from
    ensures  result == from + to
{
    assert_static from - amount >= 0    // intermediate fact
    (from - amount) + (to + amount)
}

assume

Injects a fact into the SMT context without proof. Use for FFI postconditions or OS invariants the solver cannot see. Generates warning trust-introduced unless inside a #trusted function.

#trusted
fn read_positive_from_device() -> int {
    ro v = device_read()
    assume v >= 0    // documented hardware guarantee
    v
}

calc { ... }

A structured chain of equalities (or inequalities) that guides the SMT solver step by step. Each step == expr; asserts equality with the previous line. The solver checks each step independently.

#verify
fn double_is_double(x int) -> int
    ensures result == x * 2
{
    calc {
        x * 2;
        == x * 2;
    }
    x * 2
}

More complex chains can include arithmetic identities:

#verify
fn add_assoc_proof(a int, b int, c int) -> bool
    ensures result == true
{
    calc {
        (a + b) + c;
        == a + (b + c);    // associativity — Z3 proves each step
    }
    true
}

Loop invariants

An invariant clause inside a loop body asserts a condition that holds at every iteration entry. The SMT solver checks:

1. The invariant holds before the loop (initialization).
2. If the invariant holds at iteration start and the loop condition holds, then the invariant holds at the end of the body (inductive step).

// REQUIRES_SMT_BACKEND z3

#verify
fn sum_nonneg_array(n int) -> int
    requires n >= 0
    ensures  result >= 0
{
    mut sum = 0
    mut i = 0
    while i < n {
        invariant sum >= 0
        invariant i >= 0
        sum = sum + i
        i = i + 1
    }
    sum
}

The decreases clause can also appear on a loop to prove termination:

#verify
fn countdown(n int) -> int
    requires n >= 0
    ensures  result == 0
{
    mut k = n
    while k > 0 {
        invariant k >= 0
        decreases k
        k = k - 1
    }
    k
}

Lemmas and apply

A lemma is a #verify function whose purpose is to establish a mathematical fact — it exists for its proof, not its runtime value. Typically returns bool and has ensures result == true.

// REQUIRES_SMT_BACKEND z3

#verify
lemma add_comm(a int, b int) -> bool
    ensures result == true
{
    a + b == b + a
}

The apply statement injects the postcondition of a lemma as a fact into the current SMT context. This lets you chain lemma results:

#verify
fn use_commutativity(a int, b int) -> int
    requires a >= 0 && b >= 0
    ensures  result == b + a
{
    apply add_comm(a, b)    // injects: a + b == b + a
    a + b
}

Rules:

• apply only works inside #verify functions.
• The lemma must already be proven (i.e., #verify and its contracts checked without error).
• Duplicate apply of the same lemma in the same scope is a warning W2402.

Opaque functions and reveal

#opaque

#opaque on a #pure function hides its body from the SMT solver. The solver treats it as an uninterpreted function (UF): it knows the requires/ensures contracts but not the implementation.

This prevents matching-loop divergence in recursive functions and gives control over which callers get access to the body-level proof:

// REQUIRES_SMT_BACKEND z3

#opaque #pure
fn double(x int) -> int
    requires x >= 0
    ensures  result >= 0
=> x * 2

Without reveal, a caller can only use the declared ensures (result ≥ 0), not that result == x * 2:

// EXPECT_COMPILE_ERROR contract violation

#verify
fn caller_no_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2    // Z3 cannot prove — body is hidden
{
    double(n)
}

reveal fn_name

reveal fn_name injects the body axiom of an #opaque function into the current SMT scope. After reveal, the solver can use the full body for proofs in that function:

// REQUIRES_SMT_BACKEND z3

#verify
fn caller_with_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2
{
    reveal double       // body axiom injected: double(x) == x * 2
    double(n)
}

Scope: reveal is function-local. It does not affect other callers.

Warnings:

• W2402 — reveal in a non-#verify function (no SMT context).
• W2402 — duplicate reveal for the same name in the same scope.
• W2403 — reveal for a function that is not #opaque.

#fuel(n)

#fuel(n) on an #opaque #pure recursive function enables N levels of unrolling in the SMT scope after reveal. Without fuel, the opaque body axiom is non-recursive. With #fuel(2), the solver gets two unrolling levels — enough to prove properties of small concrete inputs:

// REQUIRES_SMT_BACKEND z3

#opaque #pure #fuel(2)
fn count_down(n int) -> int
    requires n >= 0
    ensures  result >= 0
=>
    if n == 0 { 0 } else { 1 + count_down(n - 1) }

#verify
fn prove_base_case() -> int
    ensures result == 0
{
    reveal count_down
    count_down(0)      // fuel unrolls: count_down(0) == 0
}

#verify
fn prove_one_step() -> int
    ensures result == 1
{
    reveal count_down
    count_down(1)      // fuel unrolls: 1 + count_down(0) == 1
}

The fuel chain works by creating N intermediate UFs and chaining them via axioms, following Dafny’s approach.

Bounded quantifiers

Nova supports bounded quantifiers — forall/exists over concrete collections or index ranges. Unbounded universal quantifiers are a compile error.

// REQUIRES_SMT_BACKEND z3

#verify
fn all_nonneg_sum(a int, b int, c int) -> bool
    requires a >= 0 && b >= 0 && c >= 0
    ensures  result == true
{
    a + b + c >= 0
}

Syntax for bounded quantifiers in contracts:

// forall — universal
requires forall i in 0..xs.len() : xs[i] >= 0

// exists — existential
ensures  exists i in 0..result.len() : result[i] == target

The collection after in must be an iterable ([]T, range, set, map). The body must be bool and #pure.

Bit-vectors and overflow

Sized integer types — u8, u16, u32, u64, i8, i16, i32 — are encoded into the SMT bit-vector theory instead of unbounded integers. This gives precise machine semantics: arithmetic wraps around (two’s complement), and bitwise operators are reasoned about exactly.

// REQUIRES_SMT_BACKEND z3

#verify
fn low_byte(x u32) -> u32
    ensures result <= 255 as u32
=> x & 255 as u32

The plain int type stays an unbounded mathematical integer — it is not a bit-vector. Use int for general-purpose arithmetic; use sized types for low-level, packed, crypto, or FFI code where bit-width matters.

int overflow is a panic. Signed int arithmetic (+, -, *) that would exceed the 64-bit range panics at runtime — it never silently wraps. This is what makes verification of int contracts sound: the verifier reasons about int as an unbounded mathematical integer, and a proven ensures result == a + b holds for every value the function actually returns — because if a + b would overflow, the function panics instead of returning a wrong (wrapped) result. Sized integer types wrap instead of panicking (see above); reach for #nooverflow on them when wrap-around is not acceptable.

Proven-safe overflow checks are elided. Each int +/-/* compiles to an always-on overflow check (nova_int_checked_*). When the Z3 backend proves the result stays in the 64-bit range — from loop bounds, literals, or a requires — the check is removed (zero-cost), exactly like an elided bounds check (D272, same enforce-with- elision model). A loop-bounded i + j or a requires-bounded a + b emits a plain C operator; an unprovable op keeps the check (debug and release). Elision is proof- only — never triggered by #unchecked alone: a check proven only via requires is kept under --contracts=off / #unchecked(requires). Needs NOVA_SMT_BACKEND=z3; without it every op is checked. * is non-linear, so Z3 may leave it checked.

Bitwise operators &, |, ^, <<, >> are available in contracts on sized-integer operands (they remain unsupported on int).

Signedness. Unsigned types (u8/u16/u32/u64) and signed types (i8/i16/i32) differ in comparison, division, remainder and right-shift. The verifier picks the correct operator from the parameter type: i32 comparisons are signed (-1 < 0 holds), u32 comparisons are unsigned (0xFFFFFFFF > 0). Signed division rounds toward zero; >> on a signed value is an arithmetic shift.

Casts between sized types. x as u32 resizes a bit-vector: a wider target zero-extends an unsigned source and sign-extends a signed source; a narrower target truncates the low bits. For example (b as u32) where b : u8 is always <= 255, and (x as u8) keeps only the low byte.

#nooverflow

By default, sized-integer arithmetic wraps around silently. The #nooverflow attribute makes the verifier emit an extra proof obligation for every +, -, * in the function body: the operation must not overflow the type. An unprovable obligation is a compile error.

// REQUIRES_SMT_BACKEND z3

#nooverflow #verify
fn safe_add_u32(a u32, b u32) -> u32
    requires a <= 1000 as u32 && b <= 1000 as u32
    ensures  result == a + b
=> a + b

Here the precondition bounds a and b so their sum cannot exceed 2^32 - 1 — the overflow obligation is discharged. Without a bounding requires, a + b could overflow and #nooverflow rejects the function at compile time.

#nooverflow requires an SMT backend with bit-vector support (REQUIRES_SMT_BACKEND z3); the trivial backend reports the bit-vector theory as unsupported.

Trusted external functions

external fn with contracts requires #trusted. The contracts are registered as axioms — callers receive the ensures as assumptions without proof. The compiler does not verify the body (there is no Nova body to check).

#trusted
external fn libc_strlen(s str) -> int
    requires s.is_valid_cstring()
    ensures  result >= 0

#verify
fn use_strlen(s str) -> int
    requires s.is_valid_cstring()
    ensures  result >= 0
{
    libc_strlen(s)    // ensures from #trusted axiom injected
}

SMT backend selection

Nova has two verification backends:

Tests that require Z3 use the marker // REQUIRES_SMT_BACKEND z3 — the test runner skips them when Z3 is unavailable.

Timeout per function: default 2 seconds. Override locally:

#verify_timeout(10000)
#verify
fn complex_proof(x int) -> int
    ...

Cross-check verification (Z3 ↔ CVC5)

Cross-check is a CI-only soundness safety net: it re-runs every verification condition through two independent solver paths and fails the build if their definite answers disagree. It is the second line of defence after the soundness-regression suite (Plan 33.8 Ф.7) — the regression suite catches known bug classes, cross-check catches unknown ones.

The two paths are deliberately independent:

• Z3 — through the FFI backend.
• CVC5 — through a textual SMT-LIB v2 script fed to the cvc5 binary as a subprocess.

The textual path shares no code with the Z3-FFI translation, so it is also a second independent encoder. An encoding bug that silently dropped a formula on the Z3 side (the class of bug found in Plan 33.8 Ф.6.2) would be caught here even without a second solver.

Running it

# Build with the Z3 backend, install cvc5 on PATH (or point NOVA_CVC5
# at the binary), then:
NOVA_CROSSCHECK=1 nova test . --filter contracts

NOVA_CROSSCHECK=1 takes priority over NOVA_SMT_BACKEND. Normal compilation (nova build / nova check) is unaffected — it keeps using a single solver, so developer compile times do not grow.

If cvc5 is not found the run degrades gracefully to “Z3 only” with a warning — cross-check simply does not happen, the build does not break.

What counts as a disagreement

Only a definite disagreement gates: one path says Proven (unsat), the other says Disproved (sat). Any Unknown / timeout on either side is normal (the solvers have different performance profiles) and is not an error.

A disagreement is reported as compile error E2412 with the function, the VC, both verdicts, the counterexample, and the SMT-LIB script for manual reproduction. It is soundness-critical: one path produced a wrong answer, so the verifier may have declared a false Proven.

CI gate

The contracts-crosscheck workflow runs the whole contracts corpus under NOVA_CROSSCHECK=1 and requires 0 disagreements for merge. NOVA_CROSSCHECK_LOG=<file> makes every disagreement append a line to that file (the corpus is compiled process-per-file, so the file is the cross-process aggregation point the gate checks).

Contract syntax grammar

contract-clause  = requires-clause
                 | ensures-clause
                 | decreases-clause

requires-clause  = 'requires' bool-expr
ensures-clause   = 'ensures'  bool-expr
decreases-clause = 'decreases' expr

fn-contracts     = contract-clause*

loop-invariant   = 'invariant' bool-expr
loop-decreases   = 'decreases' expr

calc-block       = 'calc' '{' calc-step+ '}'
calc-step        = expr ';'
               | ('==' | '<=' | '>=' | '<' | '>') expr ';'

reveal-stmt      = 'reveal' ident
apply-stmt       = 'apply' ident '(' expr-list ')'
assert-static    = 'assert_static' bool-expr
assume-stmt      = 'assume' bool-expr

quantifier-expr  = 'forall' ident 'in' expr ':' bool-expr
                 | 'exists' ident 'in' expr ':' bool-expr

old-expr         = 'old' '(' expr ')'
result-ref       = 'result'                  // only in ensures

Attribute summary:

Error reference

Bootstrap limitations

Related documents

• spec/decisions/09-tooling.md — D24 / D89 / D111 / D112 / D113 / D114 / D116 (contracts, SMT, test tooling)
• spec/decisions/04-effects.md — D120 (#pure views + axioms), D115 (axiom binders)
• docs/plans/33.9-opaque-reveal-fuel.md — #opaque / reveal / #fuel(n) implementation (Plan 33.9)
• docs/plans/33.14-z3-cvc5-crosscheck.md — Z3 ↔ CVC5 cross-check implementation (Plan 33.14)
• nova_tests/contracts/ — ~280 contract verification tests
• nova_tests/doc/f23_contracts_positive.nv — basic contracts doc-example
• nova_tests/doc/f24_infer_contracts_positive.nv — inferred contracts doc-example
• nova_tests/doc/f25_mutation_contracts_positive.nv — mutation contracts doc-example
• nova_tests/expected_runtime/ — runtime contract violation tests (contracts_*.nv)