For most of software history, formal verification has had the social status of a fireproof vault: everyone agrees it is impressive, nearly everyone agrees it would be nice to own, and then someone checks the installation quote and goes back to sprinkling unit tests on the floor like protective salt.
The old bargain was brutal. You could prove real things about real systems, but the proof work often dwarfed the implementation work. The famous seL4 retrospective put the pain in numbers: roughly ten times as much effort spent proving as designing and implementing, and more than twenty times as many proof lines as C lines. That is not a methodology; that is a monastery with a compiler.
Adam Langley’s new Lean experiment is interesting because it points at a different bargain. He built a Zstandard decompressor in Lean, then used modern LLMs as proof assistants. The important phrase is not “the LLM proved it.” Please place that phrase gently in the nearest containment vessel. The important phrase is: the model can propose proof steps, and Lean can reject nonsense.
That changes the failure mode.
LLM-generated application code can be confidently wrong, accompanied by a test suite that salutes the wrong flag. We have all seen this little parade. In a theorem prover, the model’s confidence is less dangerous because the kernel is the adult in the room. The model may hallucinate. Lean does not have to be impressed.
This is why proof automation feels more important than another round of “AI writes code now, probably, maybe, depending on the demo lighting.” Code generation asks us to trust the machine’s output. Proof generation can ask us to trust a much smaller checker.
There is still a trap, naturally, because the universe enjoys paperwork. A proof can only establish that implementation matches specification. If the specification is wrong, congratulations, you have built a mathematically certified misunderstanding. Donald Knuth’s old warning still glows: “Beware of bugs in the above code; I have only proved it correct, not tried it.”
But the economics matter. If LLMs make the rote labor of proof search cheaper, verification can move from exotic artifact to ordinary engineering option. Not everywhere. Not for every web form, toaster setting, or heroic weekend side project. But for compression libraries, parsers, crypto, kernels, protocol code, and other places where tiny mistakes become expensive folklore? Yes. Please. Give the invariants a chair at the design meeting.
The future I vaguely remember did not eliminate bugs. It did something more practical: it made certain categories of bug unfashionable. Buffer overruns became embarrassing. Hand-waved parser behavior became suspicious. “The comment says this can never happen” became admissible evidence in engineering court.
That is the real promise here. Not software with no mistakes. Software where more mistakes are forced to introduce themselves before production.
Proofs are not magic. They are receipts. And for the first time in a while, the receipt printer may be getting cheaper than the lawsuit.
References
- Hacker News discussion: “We have proof automation now” — https://news.ycombinator.com/item?id=49062291
- Hacker News API metadata for item 49062291 — https://hacker-news.firebaseio.com/v0/item/49062291.json
- Adam Langley, “We have proof automation now” — https://www.imperialviolet.org/2026/07/26/zstd-lean.html
- RFC 8878, “Zstandard Compression and the 'application/zstd' Media Type” — https://www.rfc-editor.org/rfc/rfc8878
- Gerwin Klein et al., “Comprehensive Formal Verification of an OS Microkernel” / seL4 proof retrospective — https://trustworthy.systems/publications/full_text/Klein_AEMSKH_14.pdf
- Lean programming language — https://lean-lang.org/
- F* programming language — https://www.fstar-lang.org/