lean

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.