Kani Formal Verification Kani is a bounded model checker — it explores ALL possible values of symbolic inputs within bounds, making proofs exhaustive (not sampled like fuzzing). Critical Rules These rules prevent the most common proof failures. Violating any one will likely cause the proof to fail. No

[kani::unwind]

or

[kani::solver]

on first attempt. Omit both decorators entirely. Only add

[kani::unwind(N)]

after getting an "unwinding assertion" error, and only add

[kani::solver(kissat)]

after a timeout. Kani's defaults work better than guessing. Assert the target property inline, not via helper methods. Do not call methods that check multiple invariants or iterate over collections — they introduce loops, extra assertions, and unrelated failure points. Read the struct fields directly and write the comparison yourself: // WRONG — helper checks more than the target property, adds loops assert! ( engine . check_all_invariants ( ) ) ; // RIGHT — asserts exactly what you're proving, no extra logic assert! ( engine . x . get ( )

= engine . y . get ( ) + engine . z . get ( ) ) ; Use kani::any() without kani::assume() bounds first. Only add assume constraints after a timeout or OOM. Unconstrained symbolic values are often easier for the solver than bounded ranges. Build state through public API only. Use constructors, add_user() , deposit() , etc. Never assign struct fields directly — it creates unreachable states that cause spurious failures. The only exception is vault or similar top-level fields with no setter API. Stack allocation, not Box. Use let mut engine = Engine::new(params) not Box::new(Engine::new(params)) . Box adds heap tracking overhead to the solver. Small config parameters. If the constructor takes a size/capacity parameter that controls a loop (e.g. max_accounts ), pass a small value (4–8) that matches

[cfg(kani)]

constants found by the analyzer agent. Workflow Step 1 — Analyze the Codebase Before writing any proof, spawn an Explore agent following references/agents/kani-analyzer-agent.md . It will return loop bounds, existing infrastructure, and state construction patterns. Do not skip this. Step 2 — Write the Proof Use the agent's output to write a harness. Select a pattern from the pattern table and see references/proof-patterns.md for templates. Step 3 — Lint the Proof After writing the proof and before running cargo kani , spawn a linter agent following references/agents/kani-linter-agent.md . The linter statically detects 23 common anti-patterns (contradictory assumes, missing unwind, vacuity risks, over-constrained inputs, etc.) in seconds — far faster than the minutes-long cargo kani run. Errors → must fix before proceeding to verification (contradictory assumes, dead assertions, harness params) Warnings → should fix to avoid hangs/OOM/vacuity (missing unwind, no symbolic input, large state space) Suggestions → consider for proof quality (missing cover, assume ordering) Fix all errors and address warnings, then re-run the linter until clean before proceeding to Step 4. Step 4 — Verify and Iterate After the linter is clean, spawn a verifier agent following references/agents/kani-verifier-agent.md . It runs cargo kani , parses the output, and returns a structured diagnosis. If the verifier reports FAIL: unwinding assertion → add

[kani::unwind(N)]

with N from the error OOM → reduce symbolic ranges, lower config params, remove Box assertion failed → check the failing assertion, fix the proof logic timeout → try

[kani::solver(kissat)]

, narrow ranges covers UNSATISFIABLE → assumptions are contradictory, loosen them Iterate: fix the proof based on the diagnosis, re-run the linter, then re-run the verifier. Do not submit a proof that has not been verified. See references/kani-features.md for the full Kani API (contracts, stubbing, concrete playback, partitioned verification). Kani-Specific Concepts Non-Vacuity A proof can report SUCCESS while proving nothing. This happens when no execution path reaches assertions — because the operation always fails for your inputs, assumptions are contradictory, results are discarded, or state is empty/trivial. Detect with kani::cover!(condition, "message") — if Kani reports UNSATISFIABLE, that path is never taken. Prevent by handling results explicitly: // VACUOUS — if operation always fails, nothing is checked if result . is_ok ( ) { assert! ( invariant ) ; } // NON-VACUOUS — proof fails if operation can't succeed match result { Ok ( _ ) => { / assert properties / } , Err ( _ ) => { kani :: assert ( false , "must succeed" ) ; unreachable! ( ) } } ; Contradictory assumptions: If every path hits assume(false) or all kani::cover!() checks are UNSATISFIABLE, your kani::assume() constraints are contradictory — no valid inputs exist. Remove constraints and start unconstrained. Loop Unwinding Only relevant if you get an "unwinding assertion" error. Add

[kani::unwind(N)]

where N = max_iterations + 1. Trace ALL loops in the call graph (target + callees + constructors). Check for

[cfg(kani)]

constants that reduce collection sizes. Parameter-driven loops: If a constructor loops over a config param (e.g. for i in 0..capacity ), that param must be small (4–8). Use

[cfg(kani)]

constants when they exist. Diagnosing Failures Kani Output Fix unwinding assertion Add

[kani::unwind(N)]

with N = loop_count + 1 Timeout / solver hang Add kani::assume() to narrow ranges, try

[kani::solver(kissat)]

VERIFICATION:- FAILED Use cargo kani -Z concrete-playback --concrete-playback=print --harness name OOM / out of memory Reduce state size, remove Box, fewer symbolic variables assume(false) on all paths Remove kani::assume() constraints — they're contradictory VERIFICATION:- SUCCESSFUL Check kani::cover!() statements are SATISFIED (non-vacuity) Iterative approach: Start SIMPLE (no decorators, unconstrained inputs, API-built state) → add constraints only on timeout/OOM → add unwind only on unwinding errors → switch solver only on timeout. Proof Patterns See references/proof-patterns.md for templates. Pattern When to Use What It Proves Conservation Moves, creates, or destroys quantities Accounting equation preserved Frame / Isolation Targets one entity in multi-entity system Bystander entities unchanged INV Preservation Any state mutation Canonical invariant holds before and after Error Path Input validation / preconditions Specific error + state completely unchanged Monotonicity Counters, timestamps, accumulators Value only moves in one direction Idempotency Settlement, sync, recompute Applying twice = applying once Arithmetic Safety Numeric computation No overflow/underflow/div-by-zero Access Control Privileged operations Unauthorized callers rejected State Machine Lifecycle transitions Only valid transitions occur Inductive Delta Core accounting (strongest form) Equation holds with raw primitives Lifecycle / Sequence Multi-step user flows Properties hold through chained operations Harness Skeleton

[cfg(kani)]

mod kani_proofs { use super :: * ;

[kani::proof]

// NO #[kani::unwind] — only add after getting unwinding assertion error // NO #[kani::solver] — only add after getting timeout fn proof_name ( ) { // 1. Build state through public API (NOT field mutation) // 2. Symbolic inputs: kani::any() with NO kani::assume() bounds // 3. Call function, handle result explicitly (no if result.is_ok()) // 4. Assert ONLY the target property using raw field access // (NOT check_conservation or other aggregate methods) // 5. kani::cover!() for non-vacuity } } Codebase Preparation The Explore agent identifies what's needed. Common preparations:

[cfg(kani)] const MAX_ITEMS: usize = 4;

— reduce collection sizes [workspace.metadata.kani] flags = { tests = true } in Cargo.toml

[cfg(kani)] extern crate kani;

at crate root Reference Files references/proof-patterns.md — Pattern catalog with templates and examples references/kani-features.md — Kani API: contracts, stubbing, concrete playback, partitioned verification references/invariant-design.md — Layered invariant design methodology references/anchor-verification.md — Anchor program verification with OtterSec annotations references/agents/kani-analyzer-agent.md — Explore agent for pre-proof codebase analysis references/agents/kani-linter-agent.md — Explore agent for static lint checks (run before verification) references/agents/kani-verifier-agent.md — Explore agent for post-proof verification and diagnosis