§ Topic
kani
3 posts tagged kani.
July 31, 2026 · 9 min read
Four ways to prove a program right
Kani, Verus, Dafny, and Lean prove different things, and only one of them proves something about the binary you ship. A comparison written from the position of having used exactly one of them.
July 31, 2026 · 6 min read
Where the ghost code goes
Verus erases proofs before compilation, which sounds like a metaphor until you go read the macro that does it. What I learned about ghost types from fixing a turbofish that fell off during expansion.
July 20, 2026 · 4 min read
Proving a permutation is a bijection
A statistics library is a bad fit for testing alone. The interesting failures are index arithmetic and structural invariants nobody writes a test for — so I model-check them instead.