Table of Contents
A new wave of startups is using generative AI to make formal software verification more practical, aiming to use mathematical formulas to prove code is bug-free. While companies routinely test software for flaws, formal verification is rarely used because it is traditionally long and laborious.
The Rise of AI Verification Startups
&Truth launched publicly with $70 million in funding after research from its team used AI to verify part of the code that encrypts conversations in the messaging app Signal. Ilya Sergey, the startup’s chief science officer, compared software to bridges and buildings, noting that people use math to construct physical structures so they do not collapse.
Rival startup Harmonic, cofounded by Robinhood CEO Vlad Tenev, announced that its math-focused AI agent Aristotle supports verifying software written in C and hardware designs in Verilog. The company has received $295 million in funding and is evaluating its technology with potential users, including Nvidia and Tensordyne. Additionally, Anthropic and Theorem jointly used AI to find bugs in open source software that trillions of conventional tests missed, while also releasing an add-on for Claude to assist developers with verification.
Challenges and Skepticism
Despite high demand, experts remain divided on whether AI can push formal verification beyond critical systems at organizations like NASA and Apple into widespread use. Will Wilson, who runs the bug-hunting AI software startup Antithesis, described formal verification as a painful process and a trap for math nerds. Antithesis still uncovered additional errors using its own tool after spending millions to formally verify cybersecurity defenses, with Wilson noting that only exhaustive testing can truly prove software assurance.
Vitalik Buterin, creator of Ethereum, noted in a blog post that formal verification is not a cure-all, though proponents still view it as a crucial defense against cyberattacks launched by AI systems. Midsized tech companies also report that they typically verify only one key feature, citing a lack of verification engineers, prohibitive costs, and fears that waiting weeks for code verification could slow innovation.
Industry Adoption and Future Steps
Companies like Amazon and Apple already use formally verified software for security-related code. Byron Cook, a distinguished scientist and vice president at Amazon Web Services, stated that verification has eased cloud security concerns and helped teams fix major bugs early. Meanwhile, Proofcraft, a long-standing traditional verification provider, reported a flood of inquiries from potential customers, though leaders June Andronick and Gerwin Klein worry that AI-generated specifications could inspire unjustified trust in the results.
New entrants are continuing to enter the market, including Madan Musuvathi, who left Microsoft Research to found the startup Truidic to commercialize his studies. The general plan for verification startups is to use AI to automate the process of defining how programs should behave and translating that code into a format that math tools can check.
