/rust-formal-verification

name: rust-formal-verification
description: 'Use when Rust code, especially unsafe or panic-critical paths, needs a Kani, Verus, or Creusot harness written, run, and its failure read. Not for choosing the proof policy: use proof-driven.'
disable-model-invocation: true

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 erro