rust-formal-verification

Rust formal verification

Contract

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.