kani-proof（卡尼证明）

Prerequisites

Before writing proofs, verify tools are installed:

1. Kani: Run cargo kani --version. If missing: cargo install --locked kani-verifier cargo kani setup
2. Linter (optional but recommended): Requires Node.js. Runs via npx -p @workersio/klint klint.

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.

1. 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.
2. 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());
3. 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.
4. 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.
5. 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.
6. 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

Classify the Proof

Before choosing a workflow, classify the proof:

• Simple: Target is a pure function (no &mut self), OR pattern is P7 (Arithmetic Safety) / P11 (Concrete Known-Bad) / Safety / Equivalence, AND no loops in the call graph, AND no multi-entity state construction needed.
• Standard: Everything else — stateful mutations, P1–P6/P8–P10/P12, loops, multi-entity state.

Simple Track (no agent spawns)

For simple proofs, work inline without spawning sub-agents:

1. Write the proof directly from the pattern template. Read the appropriate references/templates/ file (e.g., arithmetic-safety.rs for P7, safety.rs for Safety/Equivalence) and adapt it. Start with references/templates/infrastructure.rs for shared macros.
2. Lint inline: Run the linter directly: npx -p @workersio/klint klint <file> Fix any errors or warnings before proceeding.
3. Verify inline: Run Kani directly: cargo kani --harness <harness_name> If it fails, apply the fixes from Diagnosing Failures and re-run.

Standard Track (with agents)

For complex proofs requiring codebase analysis, state construction, or iterative debugging:

Step 1 — Analyze the Codebase

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. Template files are available in references/templates/ — read the appropriate template and adapt it. Start with infrastructure.rs for shared macros (assert_ok!, assert_err!, snapshot types).

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

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.

When NOT to Use Kani

Kani has real limits. These situations will waste significant time on doomed proofs:

Proof Patterns

See references/proof-patterns.md for full pattern documentation. Template files are available in references/templates/ — read the appropriate template and adapt it. Start with infrastructure.rs for shared macros (assert_ok!, assert_err!, snapshot types).

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/templates/ — Rust template files for each proof pattern (infrastructure, conservation, frame-isolation, arithmetic-safety, inductive-delta, safety)
• 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