Formally Verifying the Easy Part - by Harry - Brainflow

A field report on formal verification, AI-generated code, and where the real bugs live.

Four days ago, Axiom announced a $200M Series A at a $1.6B valuation to build AI that generates formally verified code. They join Harmonic ($295M raised, $1.45B valuation) and Logical Intelligence in a funding wave totalling over half a billion dollars, all converging on the same thesis: AI will write the code, and mathematical proofs will guarantee it works. Martin Kleppmann captured the optimism well in his December 2025 prediction that AI will make formal verification go mainstream. The logic is appealing: proof checkers are incorruptible, LLMs are getting good at generating proofs, and…

saved by

• John Böllhoff

related reading

• A shallow dive into formal verificationvitalik.eth.limo
• When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
• AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com
• Automatic Formal Verification for Code Generationlogicalintelligence.com
• Prediction: AI will make formal verification go mainstream - Martin Kleppmann's blogmartin.kleppmann.com
• Asymmetry of verification and verifier’s rule - Jason Weijasonwei.net
• The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
• startup review: axiom mathil0vemilktea.substack.com
• startup review: axiom mathsubstack.com
• What Happens When the World is Run on Code No One Understands?time.com
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentsalphaxiv.org
• lf-lean: The frontier of verified software engineering | Theoremtheorem.dev