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
• Automatic Formal Verification for Code Generationlogicalintelligence.com
• AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com
• Prediction: AI will make formal verification go mainstream - Martin Kleppmann's blogmartin.kleppmann.com
• The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
• startup review: axiom mathil0vemilktea.substack.com
• How Could Formal Verification Help with Cyber Resilience?astrangeattractor.substack.com
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentsalphaxiv.org
• Your job is to deliver code you have proven to worksimonwillison.net
• The Compute Verification Postfirstscattering.com
• startup review: axiom mathsubstack.com