Three ways formally verified code can go wrong in practice

Summary

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. In formal methods, "correct" has a very specific and precise meaning: the code conforms to a specification (or "spec"). The spec is a higher-level description of what is supposed the code's properties, usually something we can't just directly implement. Let's look at the most popular kind of proven specification: -- Haskell inc :: Int -> Int inc x = x + 1 The type signature Int -> Int is a specification! It corresponds to the logical statement all x in Int: inc(x) in Int. The Haskell type checker can automati...