AI Revives 50-Year-Old Formal Verification to Check Code

A shift in AI-generated software reliability is turning decades-old formal verification into a major startup and industrial battleground, as model-generated code and mathematical proofs outpace human review. Google chief executive Sundar Pichai said at a Google Cloud annual conference this year that about 75 percent of the company's new code was written by AI before engineer approval, while Anthropic data shows more than 80 percent of its committed code was written by Claude. The productivity surge is not limited to software: on October 26, AI mathematics firm Axiom Math said teams of dozens of AI agents converted the longest proof in mathematics into 43.1 million lines of Lean-verifiable code in 24 days. Quality concerns followed. CodeRabbit found that pull requests in 470 open-source projects involving AI contained an average of 1.7 times more bugs than human-only submissions. That gap has pushed developers toward formal verification, a technique that expresses required behavior as precise mathematical specifications and then uses proof assistants such as Lean, Rocq and Isabelle to mechanically verify properties across all inputs. Unlike conventional testing, which can find defects but cannot prove their absence, formal verification offers machine-checked guarantees when specifications are correct. The method dates to the late 1960s, when de Bruijn's Automath system and Tony Hoare's program-proof logic laid the foundation. It is already embedded in high-stakes systems, including Boeing aircraft, Amazon servers and billions of Apple devices. But cost and scarcity of experts have limited it to kernels, crypto libraries and chips. The seL4 microkernel project alone consumed roughly 20 person-years. AI is changing that calculus. Because proof checkers return binary pass-or-fail feedback, models can iterate without fabricating accepted results. Stanford researcher Chuyue Livia Sun reported that a team of five humans spent eight months verifying a crypto library, while an AI system completed the remaining specifications and proofs in 11.4 hours at about $467 after receiving top-level specifications. Anthropic and Theorem later used Claude to verify 123 open-source libraries, generating about 180 million lines of proof code and uncovering hundreds of bugs missed by massive automated testing. Harmonic, founded by Robinhood CEO Vlad Tenev and backed by NVIDIA Ventures and Sequoia Capital, has extended its Aristotle prover, which reached International Mathematical Olympiad gold-medal level, to C programs and chip designs, finding deep flaws in Tensordyne hardware. Capital is flowing accordingly. Axiom, founded by Carina Hong, has raised more than $260 million and is valued above $1.6 billion; Harmonic raised $120 million in November 2025 at a $1.45 billion valuation. Startups including &Truth, Pramaana Labs and Truidic are pursuing automated code verification, regulated-industry rule checking and new verification platforms. &Truth, co-founded by Stanford professor Clark Barrett and National University of Singapore professor Ilya Sergey, aims to build a universal Lean-based verification machine, claiming AI can speed verification by 100 times and its automation by another 100 times. Yet limits remain. Verification proves compliance with specifications, not specification correctness. If AI writes code, specifications and proofs, oversight could become circular. Critics such as Antithesis founder Will Wilson warn of excessive complexity, while Ethereum founder Vitalik Buterin calls formal verification essential against AI-driven attacks but not a cure-all. With investor demand, technical progress and growing inquiry converging, the sector's decisive issue may not be proof speed but governance: who writes, validates and controls the standards that make verified AI code trustworthy.