A property test draws inputs at random. Most integer bugs live at the edges: the u64 that overflows at 2^63, the subtraction that goes negative exactly once, the comparison whose == should have been <=. Random generation finds these rarely; a bounded model checker finds all of them inside the bound.
sampling versus exhausting
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 bounds the input size. Kani then symbolically explores every input the bound admits, not a sample. If it reports no violation, the property holds for all inputs in that space, which is a claim no number of test runs can make.
The distinction is honest: a test says "I looked at a thousand cases"; a bounded proof says "there is no counterexample inside this bound." Outside the bound it says nothing, which is why the bound itself is part of the claim and belongs in the code next to the harness.
what kani checks
The technique earns its keep on arithmetic and memory-safety properties: the code paths where a wrong value is silent corruption rather than a thrown error. Counter arithmetic, saturating operations, index math, capacity checks, quorum counting: small functions whose inputs are enumerable but whose wrongness is not loud.
vhalla's spent set is the clearest instance. The set tracks which sequence numbers have been consumed; its correctness is a small-arithmetic property (a number is in the set iff it was inserted; bounds never overlap), and it is also a security boundary: a replayed sequence is a replayed message. A CI proof that the arithmetic is exact inside the bound is precisely the evidence a sampled test approximates.
Gobstopper's admission proof is the same shape: the admission decision is a comparison over bounded counters, and a Kani harness proves the comparison admits exactly the region it claims. The proof runs in CI like a test, so the arithmetic cannot quietly rot when the code around it changes.
where the proofs live
The convention keeps proofs beside the code they constrain: a #[kani::proof] harness in the crate, run by a dedicated CI job, with the bound visible in the harness. The proof is scoped to functions that are (a) deterministic, (b) free of environment calls, and (c) worth universal coverage: the arithmetic kernels where a wrong answer is silent.
That scoping is the whole discipline. Kani does not check the system; it checks named functions inside a declared bound. The proofs stay cheap because they stay small, and they stay honest because the bound and the property are code that review can read.