AI is rewriting the world's software. Who checks the math?
25–30% of code at Google and Microsoft is now AI-generated. By 2030, it could be 95%. Testing finds bugs. Mathematical proof eliminates them. This is the practitioner's guide to the verified software era.
Get the newsletterThe verification gap
AI generates code faster than humans can review it. GitHub Copilot, Claude, and GPT-4 produce syntactically correct code at unprecedented speed — but correctness and security are not guaranteed. Testing catches bugs, but it can't prove their absence.
Formal verification can. By encoding software behavior as mathematical theorems and mechanically checking the proofs, we get guarantees that hold for every possible input — not just the ones we thought to test.
The same AI that creates the verification gap can close it. Recent breakthroughs show AI agents converting production C code into Lean 4 with machine-checked proofs of correctness:
theorem zlib_decompressSingle_compress
(data : ByteArray) (level : UInt8)
(hsize : data.size < 1024 * 1024 * 1024) :
ZlibDecode.decompressSingle
(ZlibEncode.compress data level) = .ok dataAI agent converted production C code (zlib) to Lean with machine-checked proofs. Minimal human guidance. No specialized model.
Who's building the verified stack
From research labs to production infrastructure, the ecosystem is broader than most practitioners realize.
Lean FRO
Core platform, 12+ years development, 8,000+ GitHub repos. The foundation of the verified software ecosystem.
LeanDojo / Caltech
AI-driven theorem proving. LeanAgent automates proof generation. TorchLean brings verified neural networks.
AWS Cedar
Verified authorization policy engine. Production-grade, formally verified access control at scale.
Microsoft SymCrypt
Verifying core cryptographic library in Lean. Machine-checked proofs for the crypto that powers Azure.
AlphaProof / DeepMind
IMO silver medal via AI. Discovery-to-verified-proof pipeline pushing the frontier of automated reasoning.
Veil / NUS
Distributed protocol verification in Lean. Found bugs missed by two prior verification tools.
What gets verified first
Verification is spreading bottom-up through the stack, starting where correctness is most critical.
Stay ahead of the curve
A biweekly dispatch on the convergence of AI and formal verification. New research, production deployments, and what practitioners need to know. No hype. No filler.
Free. Unsubscribe anytime. No spam, ever.