Contracts and formal verification

Nova's contract system lets you state what a function requires and ensures, then verifies those claims at compile time via an SMT solver. Proven contracts are erased in release builds — zero runtime cost. Unproven ones fall back to runtime assertions in debug.

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 }
}

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

Marks a function for SMT verification. The compiler encodes the function body and all contracts as an SMT query and asks the solver. If the solver proves the contracts, they are erased in release. If not — warning W2402 + runtime fallback in debug.

#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. Contracts are kept as runtime assertions in debug; skipped in release. Use for contracts the solver cannot handle (non-linear arithmetic, string predicates, etc.).

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

#must_verify

The inverse of #unverified. If the SMT solver cannot prove the contract within the timeout, compilation fails with an error (no runtime fallback). Use for safety-critical code.

#must_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 {
    let 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. In debug — runtime check; in release — erased after being proven.

#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 {
    let 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
{
    let mut sum = 0
    let 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
{
    let 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.

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

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
    ...

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)
• 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)