Kani checks every input a small Rust function can receive within a limit you declare, where a property test only samples some of them. Most integer bugs sit at the edges: the i64 that overflows at 2^63, the subtraction that goes negative exactly once, the == that should have been <=. Random generation rarely hits those values. A bounded model checker finds all of them inside the bound.
a sample versus every input
Kani is a bounded model checker for Rust. You write a proof harness: a function that calls the code under test with kani::any() inputs, asserts a property, and optionally limits the input size. Kani then explores every input within that limit symbolically. If it reports no violation, the property holds for all of those inputs, which no number of test runs can show.
A test says “I looked at a thousand cases.” A bounded proof says “there is no counterexample inside this bound,” and nothing about inputs outside it. That makes the bound part of the claim, so it belongs in the code next to the harness.
which functions get a proof
Kani pays off on arithmetic and memory-safety properties, where a wrong value corrupts data silently instead of raising an error: counter arithmetic, saturating operations, index math, capacity checks, and quorum counting. These are small functions whose inputs can be enumerated.
vhalla’s spent set is the clearest example. It tracks which sequence numbers have been consumed. Its correctness is a small arithmetic property (a number is in the set if and only if it was inserted, and ranges never overlap), and it also protects security, because a replayed sequence number means a replayed message. A CI proof that the arithmetic is right for every value inside the bound is the evidence a sampled test can only approximate.
Gobstopper’s admission proof has the same shape. Gobstopper decides whether to accept a request by comparing counters with fixed limits, and a Kani harness proves the comparison accepts exactly the region it claims. The proof runs in CI like a test, so the arithmetic cannot drift unnoticed when the surrounding code changes.
how the proofs run
Each proof sits beside the code it constrains as a #[kani::proof] harness in the crate, runs in a dedicated CI job, and shows its bound in the harness. Proofs are written only for functions that are deterministic, make no environment calls, and are worth checking for every input: the arithmetic kernels where a wrong answer is silent.
Kani checks named functions inside a declared bound, never the whole system. Keeping the proofs small keeps them fast, and because the bound and the property are code, a reviewer can read exactly what was proved.