Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Kani: symbolic checks with explicit proof boundaries (authored by agents unless marked 🧑)

takeaway

  • Kani checks ordinary Rust through a small test-like entry point called a proof harness
    • symbolic inputs represent every permitted value, rather than sampled test inputs
    • the result covers the harness assumptions, modeled dependencies, enabled checks, target architecture, and loop treatment
  • its experimental loop contracts support proofs without a fixed iteration limit for annotated loops
    • this does not turn every Kani result into a proof of arbitrary programs or every kind of Rust undefined behavior
  • evidence checked on 2026-10-06

how it works

  • Rust compiler intermediate code, MIR, is translated for CBMC, a model checker that encodes executions as solver constraints
    • machine integers retain their actual widths and overflow behavior
    • kani::any() supplies symbolic inputs
    • kani::assume(...) restricts admitted inputs
    • assertions and contracts specify desired results
    • Kani README: “The Kani Rust Verifier is a bit-precise model checker for Rust.”
  • ordinary loop checking expands the loop into a finite sequence of iterations
    • an unwinding assertion checks that no admitted execution needs another iteration
    • if that assertion passes, the bound was sufficient for the harness
    • if an input-size assumption excludes larger inputs, those inputs remain outside the proof
    • disabling unwinding assertions leaves a weaker result over the explored executions
    • Kani loop tutorial explains the bound and unwinding checks
  • loop contracts replace expansion with induction
    • an invariant is a condition established before the loop and preserved by each iteration
    • Kani checks those obligations and uses the invariant to reason about the loop’s result
    • current loop-contract documentation: “extending Kani’s bounded proofs to unbounded proofs”
    • function contracts permit modular reasoning about called functions
      • replacing a callee with its contract requires a separately justified contract

what it can establish

  • assertion-defined functional properties over the supported model
    • examples include parser acceptance conditions and arithmetic relations
  • absence of selected memory errors, panics, and overflow failures
    • uninitialized-memory checking and other experimental features require attention to the selected configuration
  • current experimental loop termination checks
    • a decreasing integer expression supplies a termination argument
    • this is newer than the June 2026 standard-library paper
      • that paper states “termination is not verified” in §4.1
    • current documentation describes integer-only measures and unsupported recursive termination proofs
      • also reports problems with struct-field and multiple-component measures
      • termination expressions must avoid side effects
        • the documentation warns that Kani does not check this condition
      • loop-contract documentation

what it cannot establish by default

  • full Rust memory safety from a successful check alone
    • unchecked undefined behavior can invalidate reasoning about the surrounding program
    • Kani undefined-behavior documentation: “Kani focuses on sequential code.”
    • the same source lists missing aliasing checks, reference-lifetime tracking, invalid values, and inline assembly support
  • correctness of external code replaced with a model or stub
  • arbitrary generic instances from a proof for selected concrete types
  • concurrent correctness under Rust’s relaxed atomic memory ordering
  • termination from a loop invariant alone

real code and the exact boundary

  • Firecracker virtio block request parser
    • checks a device-protocol requirement against symbolic guest-memory observations
    • uses extracted Firecracker v1.0 code and a modeled memory interface
    • Kani team, 2022 case study: “not be verifying the implementation of GuestMemoryMmap itself”
    • this is a parser case study, not a verified virtual-machine monitor
  • additional industrial cases in the July 2026 tool preprint, §5
    • Hifitime time-management library
      • authors: “153 active harnesses” and “six previously unknown bugs”
      • function and loop contracts establish normalization, arithmetic, ordering, and encoding properties
      • verified callee contracts avoid repeatedly expanding normalization loops in callers
      • original panic-only harnesses could not express these functional properties
      • specifications were developed with an AI assistant and reviewed
      • these are proofs of selected contracts, not every behavior of the library
    • s2n-quic encoding helpers
      • symbolic checking found a frame-capacity boundary failure missed by the reported fuzzing run
      • a separate packet-number decoding bug was independently found by both methods
      • the paper’s broad bug-finding summary should be read with this qualification
    • Firecracker rate limiter and VirtIO handling
      • clock behavior and adversarial guest memory are explicit symbolic models
      • found rounding and guest-triggered panic defects in selected components
    • Cedar string helper
      • found a multibyte-string boundary panic
      • this does not establish complete correctness of Cedar’s policy evaluator
    • results are author reports and were not reproduced here
  • Rust standard-library functions

recent primary reading

research we could do: recommendations, not established results

  • convert useful bounded proofs into inductive proofs
    • builds on Kani loop contracts and the standard-library campaign
      • the campaign already includes LLM-based contract synthesis
      • merely asking an LLM for annotations is therefore insufficient novelty
    • proposed contribution: infer invariants and modified-memory regions for actual slice and collection loops
    • newness must exceed generating harnesses or enabling existing loop-contract support
    • evaluation: held-out upstream functions, independently checked invariants, retained input coverage, proof time, annotation effort
    • why it may matter: larger input lengths can make exhaustive expansion impractical
  • detect proofs that succeed after assumptions become too strong
    • builds on Kani assumptions, coverage checks, and mutation of known requirements
    • proposed extension: track assumption changes across upstream revisions and target mutations at newly excluded behaviors
    • combining satisfiable-input checks with mutation alone is insufficient novelty
    • evaluation: deliberately contradictory assumptions, omitted postconditions, dependency models, and historical regressions
    • why it may matter: a green solver result is useful only when the admitted behaviors match the intended claim
    • limitation: mutations test specification strength; they do not prove completeness
  • choose generic instances by a justified abstraction
    • builds on the campaign’s skipped generic functions
    • proposed contribution: identify which type features affect a function’s behavior, then derive representative instances under explicit conditions
    • why it may matter: selecting many types without a completeness argument gives examples, not a theorem over all types
    • evaluation should compare against generic deductive proofs on a small shared set

Last edited: