§ Topic
verus
2 posts tagged verus.
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.