Break the proof
The gate below is the same function the contract runs, compiled for your browser. Each copy on the right has one rule taken out. Pick an attack and a copy.
Loading the gates.
What this shows, and what it does not
The Lean theorems are proved about a model of the gate written in Lean from the Rust function; they do not read the Rust. Two checks tie the model to the code: Kani checks the same properties on the Rust function itself for every input its harness allows, and a test runs the Lean model and the Rust function on 2,000 fixed cases and compares every answer. None of this covers the rest of the contract: storage, the address book proofs, the ledgers' bookkeeping, signatures, the agent, the model or the chain.