rust-formal-verification git:20260905.f02db66A

Immutable. This exact content is served forever at /api/v1/blob/bc27807c29c216b3.

---
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.'
---

# 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.