Kani: A Model Checker for Rust

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and result

This paper presents Kani, a Rust model checker that turns proof harnesses and contracts into CBMC GOTO programs and bit-precise SAT/SMT queries. Its practical method is a progression: start with exhaustive bounded checks for panic, undefined behavior, and assertions; add inductive loop and function contracts when unwinding is too expensive; use quantified invariants and verified stubs to compose proofs. The paper says Kani “pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties” (abstract, p. 1). The guarantee is conditional on harness coverage, explicit assumptions, sound contracts or stubs, and several unsupported semantic features.

The workflow is concrete. Put a #[kani::proof] harness in a Cargo crate, generate arbitrary typed values with kani::any, constrain only valid caller states with kani::assume, and assert the property. Run cargo kani; Kani reuses rustc through MIR, instruments Rust safety checks, lowers MIR to CBMC GOTO, and asks a SAT or SMT solver for a counterexample. A satisfiable formula gives a concrete failing execution; an unsatisfiable formula proves all checked paths up to the unwind bound. The paper’s architecture description is explicit: “Kani compiles Rust’s MIR into CBMC’s GOTO program representation, inheriting bit-precise arithmetic and memory reasoning” (section 4.1, p. 4).

technique: bounded harness model checking

Use this first for panic freedom, memory and validity safety, arithmetic assertions, and finite loops. It is push-button because Kani inserts checks for invalid or dangling dereferences, misaligned casts, invalid enum discriminants, overflow, division by zero, undefined shifts, bounds errors, unwrap on None, and selected resource properties. Two deeper MIR passes check valid-value coercions and uninitialized memory, but they are opt-in because of solver cost.

Steps:

1. Write a harness with #[kani::proof] and obtain symbolic inputs: let x: u64 = kani::any();.
2. State real preconditions with kani::assume(x > 0 && y > 0). Never use assume(false) to silence a failure. Kani warns that “an incorrect assumption (e.g., assume(false)) makes the proof vacuously true, so assumptions must be reviewed as carefully as the code itself” (GCD example, p. 2).
3. Call the implementation and use assert! for the required behavior.
4. Give every loop a bound with #[kani::unwind(k)]. Kani adds an unwinding assertion after the final copy. A passing safety assertion with a failing unwinding assertion is inconclusive, not a proof.
5. Inspect the counterexample and source location; replay it with Kani’s concrete playback support or as an ordinary Rust test.

The paper’s GCD harness uses #[kani::unwind(94)], arbitrary positive u64 inputs, and assert!(d != 0 && x % d == 0 && y % d == 0). The 94 bound follows the 93-iteration worst case for 64-bit Euclid. This is mathematically complete for that loop, but the full-range formula did not finish within one hour. Thus a finite bound can be sound and still unusable. For input-dependent loops there may be no tractable bound.

Verus form (inference): a Verus proof would write a requires clause and ensures clause on the function and prove a loop invariant with invariant; it would not use kani::any or an unwind annotation. Kani’s inserted panic and validity checks are checked automatically up to the bound; in Verus the analogous obligations (e.g. no arithmetic overflow, per the SAFE paper, section 4.3.2) are also generated automatically but must be proved for all inputs, so annotations such as invariants may be needed. This inference follows from the paper’s description of Kani’s inserted checks and the SAFE paper, not from a Verus experiment.

Evidence and limits: the paper reports eleven bugs missed by testing and fuzzing across four production Rust codebases. One s2n-quic bug survived 16,777,216 fuzz executions but Kani found it in 20 seconds; another was found in 2.8 seconds. These are bug counts and executions, not a probability that Kani finds bugs. Bounded results cover only paths represented by passed unwinding assertions. Generic code is checked per monomorphization; dynamic dispatch, concurrency, and some FFI remain outside the claimed model.

technique: function contracts and compositional abstraction

Use contracts when callers should rely on a function’s behavior without rechecking its loops. A contract has requires(P), ensures(|r| Q), and an inferred or explicit modifies write set. Expressions must be deterministic, side-effect free, and allocation free. old(e) refers to the pre-state in an ensures clause, which is needed for &mut parameters. For example, ensures(|r| *v == old(*v) + 1) specifies an increment.

Application steps:

1. State the weakest useful precondition and a postcondition strong enough for callers. Kani checks both the result and a frame condition outside Mod.
2. Add #[kani::proof_for_contract(f)]. Kani creates arbitrary ownership-valid arguments, assumes the precondition, executes f, asserts the postcondition, and checks writes.
3. If the body contains loops, provide loop contracts so the contract proof does not depend on an unwind bound.
4. At callers, use #[kani::stub_verified(f)]. Kani asserts the precondition, havocs the permitted write set, and assumes a nondeterministic return satisfying the verified postcondition.

The GCD contract uses requires(x > 0 && y > 0) and ensures(|&result| result > 0). Its loop invariant preserves positivity and equality of the common-divisor sets of original and current pairs. The paper deliberately uses the weaker positive-result postcondition because “Z3 cannot automatically instantiate the quantifier at d = result over nonlinear 64-bit bitvector remainder” (section 2.2, p. 3). The contract proof passes all 202 checks in 0.54 seconds with Z3. In the TokenBucket caller, replacing GCD by its verified contract changes hours of contextual unwinding to seconds over all 64-bit inputs.

For mutable references, Kani infers locations reachable through &mut T; an explicit modifies clause can narrow the set. Raw pointers require modifies, because Kani cannot infer their reachable memory. The frame rule assumes locations inside and outside the write set do not alias. Safe Rust borrow checking supplies this assumption for safe code; unsafe callers must establish aliasing closure themselves.

Verus form (inference): write requires and ensures; Verus has no modifies clause, and writes are limited by the &mut ownership a function receives; Verus ensures refers to the pre-state of a &mut parameter with old(x), so no snapshot is needed. Verus can express richer ghost-state relations but normally requires more annotations. Kani’s verified-stub abstraction is analogous to proving a lemma once and using its specification at calls, while plain Kani stubs remain trusted models.

Failures and assumptions: a too-strong precondition makes a contract unusable at legitimate callers; a weak postcondition may not prove the caller’s property. Recursive contracts provide partial correctness by induction, but Kani does not verify recursive termination; mutual recursion is rejected. Panics are assertion violations, so successful contracts include panic freedom under their precondition. The trusted boundary includes harness reachability, termination for recursion, unsafe aliasing, sequential execution, and FFI behavior.

technique: inductive loop contracts

Use loop_invariant(I), loop_modifies(W), and loop_decreases(d) when exhaustive unwinding is too costly or impossible. Kani checks the Floyd–Hoare obligations: invariant at entry, preservation under I && guard, writes within W, and invariant plus exit condition after the loop. Its transformation executes the loop body twice: once for the base case and once for the inductive step, with havoc of the write set between them. Verification time is independent of iteration count.

Steps:

1. State an invariant strong enough to imply the function postcondition when the guard is false.
2. Add loop_modifies when Kani cannot infer the exact write set.
3. Add a non-negative integer loop_decreases measure. Kani proves it decreases on every guarded iteration; without it, only partial correctness is established and Kani warns.
4. For nested loops, prove the inner abstraction first and ensure its write set is contained in the outer write set.

The GCD code uses loop_invariant(a > 0 && forall d in (1, a.saturating_add(1)) ... ) to preserve common divisors and loop_decreases(b) because a % b < b. The base case is the initial (x,y) pair; the inductive step follows Euclid’s divisibility identity; at exit b == 0, so positivity implies the selected postcondition. A Hifitime Mul<f64> loop uses p >= 0 && p <= 19 and loop_decreases(19i32.wrapping_sub(p)); it verifies in 0.2 seconds versus 91.8 seconds for 19-step unwinding, and Mul<f64> verification in the full-crate context completes in under 70 seconds with the contract (intractable without it).

Verus form (inference): use while with invariant clauses and a decreases clause. Quantified invariants may need trigger annotations or auxiliary lemmas in Verus; Kani passes quantifiers to Z3 or expands finite ranges. Kani currently supports only simple integer decreases expressions, not lexicographic tuples or general well-founded orders. Custom iterators require an abstraction; range-based for loops are rewritten exactly by Kani.

technique: quantifiers

Use kani::forall!(|x: T in (lo, hi)| P(x)) and kani::exists! for properties over bounded domains, including the GCD divisor relation. SAT backends eagerly expand ranges and require compile-time bounds; Kani warns above 1000 values. Z3, cvc5, and Bitwuzla receive first-order formulas and allow runtime-valued bounds, but solver instantiation can fail, as the GCD postcondition demonstrates. Keep ranges finite and choose a solver intentionally with #[kani::solver(z3)].

Verus form (inference): use quantified specifications and lemmas, with explicit triggers and arithmetic lemmas where the SMT solver cannot instantiate a useful witness. Kani’s range syntax and backend behavior do not transfer directly.

technique: function stubbing

Use #[kani::stub(f, g)] to replace unsupported, expensive, or environmental code in one harness. Kani checks parameter, return, and generic-arity compatibility at compile time. Typical uses are FFI, inline assembly, system clocks, random values, and large implementations. A plain stub is handwritten and unchecked against f; its behavior is therefore trusted. stub_verified is stronger: Kani first verifies a contract and then applies the contract abstraction.

The Firecracker rate limiter stubs libc::clock_gettime with monotonically non-decreasing nondeterministic Instant values, exposing adversarial timing symbolically. This found a rounding bug allowing up to 0.01% bandwidth excess. The paper stresses that a plain stub is sound only if it over-approximates every replaced behavior. VL should treat environmental stubs as explicit trusted models and record their assumptions.

evidence, trust, and product implications

Hifitime began with 11 panic-freedom harnesses. A 2024 expansion reached 168 harnesses (section 5.2, p. 8; “through a combination of manual and automated harness generation”), and 158 of the 168 were automatically generated, so the two counts are different sets (11 original plus 158 is 169, not 168, and the paper does not reconcile this); 57 of the 158 generated harnesses timed out at 60 seconds because every caller re-unrolled normalize. Contract-based Phase II used 84 ensures, 41 requires, 12 converted contract harnesses, 61 new contract harnesses, and 80 standalone proofs: 153 active proofs. Table 3 reports six property classes: normalization, algebraic laws, encode–decode, calendar validity, loop termination, and specification consistency. The contract phase found six new bugs, namely a total_nanoseconds() sign error, an i64::MIN.abs() panic, a NaN-loop failure, an Epoch PartialEq/Ord inconsistency, a Duration PartialEq/Ord zero-crossing inconsistency, and an is_gregorian_valid overflow (section 5.2.2).

CI scale is broad but self-selected. Table 1 gives 34 Firecracker harnesses in 21 minutes, 102 s2n-quic in 23 minutes, 153 Hifitime in 42 minutes, 16,748 standard-library harnesses in 69 minutes, and smaller projects from 1 to 22 harnesses. The paper’s claim that Kani is sustainable follows these deployments, not a random sample. The authors state that “the evaluated projects self-selected into Kani adoption, potentially over-representing favorable cases” (section 5.3, threats to validity, p. 10).

What is proved: passed bounded checks prove assertions for all executions within a complete unwind; verified contracts and loop invariants provide unbounded functional or termination guarantees under their premises; solver verdicts come from CBMC with a SAT/SMT backend, which the paper does not certify. What stays trusted: Rust compiler and MIR-to-GOTO translation, solver correctness, harness coverage, user assumptions, plain stubs, unsafe pointer aliasing, recursion termination, FFI models, and the sequential/no-async execution model. Kani does not model Stacked Borrows or Tree Borrows aliasing, which the paper calls “the primary class of UB in unsafe Rust” and, with FFI, one of the two most significant assumptions in practice; Miri is suggested as a complement.

Threat to a product built from agent-written verified Rust (inference): Kani is a useful exhaustive gate for generated panic and memory-safety behavior and a scalable way to reject counterexamples before release. Agents can still write vacuous assumptions, weak postconditions, unsound stubs, or invariants that prove only partial correctness. Product claims should therefore record unwind completeness, contract and stub provenance, solver/timeouts, and unsupported concurrency or aliasing. Verus remains preferable for richer ghost-state and data-structure proofs; Kani’s strength is low-annotation bit-precise exploration and compositional contracts.

What VL should not redo: the paper already establishes the MIR-to-CBMC architecture, GCD bounded-versus-contract comparison, verified-stub rule, quantifier backend tradeoffs, and an industrial Hifitime migration with exact harness counts and timings. New work should test product-specific assumptions, especially agent-generated contracts, unsafe aliasing, concurrency, and environmental models, rather than repeat generic GCD demonstrations.

techniques for the catalog

• bounded proof harnesses — use kani::any, checked assumptions, assertions, and a complete unwind bound to exhaustively check finite executions and Rust safety properties
• function and loop contracts — prove preconditions, postconditions, frame conditions, invariants, and integer decreases measures, then reuse verified behavior compositionally
• quantified specifications — express forall and exists over finite or SMT ranges, selecting a backend while checking instantiation and range cost
• verified and environmental stubs — replace a proved callee by its contract, or model FFI and clocks with explicit trusted nondeterministic abstractions

Audited 2026-10-12 against the paper: checked GCD numbers (94, 93, 202 checks, 0.54 s, one hour), the specification grammar and rules, loop-contract transformation, Table 1 (harness counts, runtimes), Tables 2-3, Hifitime counts (11, 168, 158, 57, 84, 41, 12, 61, 80, 153), timings (0.2 s, 91.8 s, 70 s), s2n-quic and Firecracker figures, and quotations. Changed: page/section of three quotations, Hifitime bug list, full-crate timing scope, trust-boundary wording, and two Verus-form statements (Verus has old(x) and automatic overflow obligations). Not checked: the 0.01% Firecracker figure beyond the paper’s text; no external check of Kani behavior. Follow-up: Hifitime 168 versus 158 confirmed as not a conflict (158 generated of 168 total) but the paper’s 11 + 158 = 169 against 168 is unreconciled, stated in one clause.

Last edited: 2026-10-13