Rust formal verification

Contract

Field	Bound contract
Trigger	A Rust function or module needs bounded model checking (Kani) or deductive verification (Verus, Creusot) against explicit properties, or an existing harness fails and its counterexample must be read.
Authority	Reversible local: writes proof harnesses, contract attributes, and spec functions inside the crate, plus a Cargo.toml dev-dependency or feature for the verifier; rollback is reverting those files. No remote mutation.
Side effect	Harness and annotation source in the crate, the verifier's build artifacts under target/, and for Kani concrete-playback unit tests when requested.
Done	Every named property has a harness or contract that the chosen tool reports as passing under a recorded bound, or a counterexample mapped to a code defect and a fix.

Inputs

The crate, the functions in scope, and the properties: absence of panics and overflow, memory safety of unsafe blocks, or functional pre- and postconditions. Tool pins from the grounded set: Kani kani-0.67.0 (cargo install --locked kani-verifier && cargo kani setup; Kani tracks a pinned Rust nightly, not stable), Verus rolling release release/0.2026.08.30.b432e82 (download the release zip from GitHub Releases and run ./verus, which installs its pinned toolchain through rustup when missing), Creusot v0.13.0 (git clone the repo and run ./INSTALL, which needs cargo, opam, and curl, and installs why3 and why3find provers). Optional: an unwind bound per loop, and a solver choice.

Procedure

1. Pick the tool by the property. Kani answers "does this code panic, overflow, or violate memory safety for any input up to a bound" and needs no specification language, so it is the default. Verus answers "does this function meet its requires and ensures for all inputs" and needs the code written inside the verus! macro with spec fn and proof fn alongside exec fn. Creusot answers the same question for ordinary Rust with #[requires] and #[ensures] attributes and discharges obligations through Why3. Prusti is a deprioritized fallback: its last release is v-2024-03-26-1504 (2024-03-26), so reach for it only when a codebase already carries Prusti annotations. Done when: one tool is named with the property class that chose it.
2. Write a Kani harness. Add kani as a conditional import and write, next to the code under test, #[kani::proof] fn check_name() { let x: u32 = kani::any(); kani::assume(x < 1000); let r = f(x); assert!(r <= x); }. kani::any() yields every value of the type; kani::assume narrows the domain and is the harness precondition; assert! is the property. Add #[kani::unwind(N)] on a harness whose code loops, with N large enough that the unwinding assertion passes; Kani then reports whether the bound covers every iteration the inputs allow. Use kani::cover!(cond, "msg") to confirm a branch is reachable, so an assume has not emptied the input space. For a function expected to panic, mark the harness #[kani::should_panic]. Done when: the harness compiles under cargo kani --harness check_name and at least one cover is SATISFIED.
3. Run Kani and read the result. cargo kani runs every harness; --harness NAME runs one; --default-unwind N sets a global loop bound; --output-format terse shortens the report. The report lists Check N: <harness>.<class>.<n> blocks, each with Status: SUCCESS|FAILURE|UNREACHABLE|UNDETERMINED, a Description, and a Location, then a SUMMARY and the final line VERIFICATION:- SUCCESSFUL or VERIFICATION:- FAILED. A FAILURE whose description is an unwinding assertion means the bound is too small, not that the code is wrong; raise unwind and rerun. A FAILURE on an assertion, overflow, or pointer check at a source location is a defect candidate. Turn it into a test with cargo kani --harness NAME -Z concrete-playback --concrete-playback=print, which prints a Rust unit test with the concrete inputs; inplace writes it next to the harness. Run that test under plain cargo test to confirm the failure is real. Done when: every check is SUCCESS or its failure is reproduced by a concrete test.
4. Add Kani contracts when the bound does not scale. With -Z function-contracts, annotate the callee with #[kani::requires(...)] and #[kani::ensures(|result| ...)], verify the contract with a #[kani::proof_for_contract(f)] harness, and let callers use #[kani::stub_verified(f)] so their harnesses see the contract instead of the body. With -Z loop-contracts, write #[kani::loop_invariant(cond)] above a loop to replace unwinding with an inductive argument. Done when: the caller's harness passes without an unwind bound on the stubbed callee.
5. Write and run Verus. Wrap the module in verus! { ... }. Give each exec fn its requires and ensures clauses; write the pure logic as spec fn with int and nat, and give every recursive spec fn a decreases clause. Move helper reasoning into proof fn lemmas and call them from the code. Use assert(P) by { ... } to scope a local sub-proof so only P survives into the context. Run verus file.rs; add --verify-module m or --verify-function f to narrow the run, --expand-errors to have Verus split a failing postcondition into the conjunct that fails, --rlimit N to change the SMT resource limit (default 10), and --time to see where verification time goes. Success prints verification results:: N verified, 0 errors; a failure is a rustc-style error: ... failed with a source span. Exit code is 0 on success and 1 on any verification or compile error. Done when: the module reports zero errors, or the failing conjunct is named by --expand-errors and traced to code or spec.
6. Write and run Creusot. Annotate with #[requires(...)], #[ensures(...)], loop #[invariant(...)], and #[variant(...)] for termination; #[trusted] skips a body and is a stated assumption, so list every use in the output. Inside Pearlite specs, @ views a Rust value as its mathematical model (x@ for an integer), ^ is the final value of a mutable borrow, and ==> is implication. Run cargo creusot to compile the crate to Coma and run the provers; --only=coma skips proving and --only=prove skips compilation. On an unproved goal, open the Why3 IDE with cargo creusot -i (or --ide-always) and step through the goal to find the missing invariant or lemma. Done when: every goal is proved, or the unproved goal is named with the invariant that is missing.
7. Record the result. For Kani, write the unwind bound and the solver beside each harness; a pass at unwind(8) is a proof for inputs within that bound, and nothing beyond. For Verus and Creusot, list every #[trusted] body and every assumption the tool admitted without proof; each one is an obligation the reader must accept. Done when: the output names the bound and the trust set for each property.

Failure and recovery

On a Kani build failure mentioning the toolchain, rerun cargo kani setup; Kani's nightly pin is independent of the crate's rust-toolchain. On a Kani run that does not finish, lower the bound with --default-unwind for a first result, then split the harness by input region with kani::assume. On UNDETERMINED or UNREACHABLE checks, inspect the assume chain: an empty input space makes every assertion vacuous, and a cover that is UNSATISFIABLE proves it. On a Verus quantifier problem (a proof that times out or depends on trigger choice), run with --triggers-mode verbose to see the automatically chosen triggers and restate the quantifier so that a stable trigger term exists; do not raise --rlimit without recording why. On a Creusot goal that Why3 cannot close, add a loop invariant or a lemma rather than #[trusted]; a #[trusted] added to make the run green is a defect in the report. On a Prusti request, state its release date and ask whether the Kani or Verus path is acceptable before writing Prusti annotations. When a property cannot be discharged at any useful bound, report the bound reached, the tools tried, and the obligation left open; do not narrow the property.

Output

Harness or annotated source in the crate; per property, the tool, version, bound or resource limit, and verdict; for each failure, the concrete counterexample test (Kani) or the named failing conjunct or goal (Verus, Creusot) with the code or spec fix; the list of every remaining trusted or assumed obligation.