October 10, 2025
Three ways formally verified code can go wrong in practice
"Correct" doesn't mean "correct" when correctly using "correct"
New Logic for Programmers Release!
v0.12 is now available! This should be the last major content release. The next few months are going to be technical review, copyediting and polishing, with a hopeful 1.0 release in March. Full release notes here.
Three ways formally verified code can go wrong in practice
I run this small project called Let's Prove Leftpad, where people submit formally verified proofs of the eponymous meme. Recently I read Breaking “provably correct” Leftpad, which argued that most (if not all) of the provably correct leftpads have bugs! The lean proof, for example, should render leftpad('-', 9, אֳֽ֑) as ---------אֳֽ֑ , but actually does ------אֳֽ֑ .
You can read the article for a good explanation of why this goes wrong (Unicode). The actual problem is that correct can mean two different things, and this leads to confusion about how much formal methods can actually guarantee us. So I see this as a great opportunity to talk about the nature of proof, correctness, and how "correct" code can still have bugs.
What we talk about when we talk about correctness
In most of the real world, correct means "no bugs". Except "bugs" isn't a very clear category. A bug is anything that causes someone to say "this isn't working right, there's a bug." Being too slow is a bug, a typo is a bug, etc. "correct" is a little fuzzy.
... continue reading