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