Nitpick Formal Verification & Design by Contract

Nitpick’s fundamental philosophy is the rejection of unsafe behavior. To achieve this, it deeply integrates with the Z3 SMT solver to mathematically prove the correctness of the code before it is allowed to execute.

1. Static Assertions

The assert_static builtin allows developers to encode compile-time logic checks. If the expression evaluates to false, compilation immediately halts.

assert_static(1i32 == 1i32);

2. Formal Proofs (prove)

The prove keyword interacts directly with the Z3 verification backend (when the --verify compiler flag is set). It forces the SMT solver to construct a mathematical proof that the subsequent expression holds true across all possible control flows and variable states.

If the solver finds a path where the expression is false, compilation fails. The compiler extracts a counterexample showing the failing variable assignments (visible via --prove-report).

int32:x = get_val();
if (x > 0) {
    prove(x != 0); // Mathematically verified at compile time.
}

2.1 Path Condition Accumulation (v0.66.1)

The prove keyword is path-condition-aware: branch guards from enclosing if, while, and other control flow are accumulated and asserted as Z3 axioms before checking the proof obligation. This means prove(x != 0) inside if (x > 0) automatically benefits from the guard x > 0.

3. Loop Invariants (invariant)

Loop constructs (loop, while, till, when) accept an optional invariant clause that specifies conditions the verifier must prove hold at every iteration.

Rules<int32>:r_pos = { $ > 0i32 };
limit<r_pos> int32:sum = 1i32;

while (sum < 100i32) invariant sum > 0i32 {
    sum = sum + 1i32;
};

When compiled with --verify-contracts, the compiler proves the inductive step: given that the invariant holds at the start of an iteration and the loop condition is true, the invariant still holds at the end of the iteration.

4. Limit Rulesets

The limit<Rules> keyword allows developers to bind strict structural constraints to types. These constraints are heavily analyzed by the verifier to ensure physics boundaries or contract bounds are not breached during runtime execution.

(See contracts_limits_specs.txt for extensive examples on Rules limits and Design by Contract features like requires and ensures.)

5. Z3 Borrow Checker Integration (v0.66.6)

The borrow checker leverages Z3 to prove index disjointness for array borrows. When two mutable borrows ($$m) target the same array but use index variables constrained by different limit<Rules>, Z3 can prove the indices are always unequal, suppressing false-positive aliasing errors.

Rules<int32>:EvenIdx = { $ % 2i32 == 0i32 };
Rules<int32>:OddIdx  = { $ % 2i32 == 1i32 };

func:update_interleaved = int32(
    limit<EvenIdx> int32:i, limit<OddIdx> int32:j,
    int32[100]:arr
) {
    $$m int32:a = arr[i];   // mutable borrow at even index
    $$m int32:b = arr[j];   // Z3 proves i != j → no aliasing error
    pass(a + b);
};

6. Verification Compiler Flags

7. Verification Backends

Nitpick has two complementary verification systems:

• Z3 SMT Solver (compile-time): Decides concrete proof obligations for a specific program during compilation.
• K Framework / kprove (metatheory): Proves properties about the language semantics themselves, offline during language development.

(See VERIFICATION_BACKENDS.md in the Nitpick repository root for the full architectural documentation.)