Kani's first run on my crate caught a real bug: adversarial decodes broke a proven merge law

[KyleClouthier]

I wanted to share a Kani success story from bitrep, an open-source crate for order-invariant, bit-identical float reductions (https://github.com/KyleClouthier/bitrep).

The setup: the crate's merge algebra is proved in Lean 4 at the spec level (merges commute and associate, codecs are inverses). But a proof about the spec says nothing about my Rust. So Kani harnesses check the implementation symbolically on every push: merges commute, merges associate, encode/decode round-trips, for all inputs.

The catch: on the first run against the v0.2 decoder, Kani found that adversarially crafted byte strings could decode into states that violated the merge laws. The Lean proof was fine, the honest-encoder path was fine, but the decoder accepted non-canonical states that the spec's invariants assumed impossible. Exactly the class of bug that testing with honestly-encoded inputs can never find, because the bug only exists for inputs no honest encoder produces.

The fix: the decoder now rejects non-canonical states, and the rejection itself is under a Kani harness.

Setup that might interest others: six harnesses run in CI on every push alongside a Lean axiom audit and differential fuzzing against a big-integer oracle. The division of labor is explicit: Lean owns the algebra, Kani owns the implementation's conformance to it, the fuzzer owns the numerical semantics against an independent oracle. Harnesses are in the repo under verification/.

Thanks for the tool. Happy to answer questions about the setup, and open to suggestions on harness patterns I should add.

[feliperodri]

That is such a great story!! Would you be interested to write a blog post about it for our Kani Blog? All you have to do is to submit a PR with your story here: https://github.com/model-checking/kani-verifier-blog