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.