Startups Bet AI Can Scale Formal Verification
Original: The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
Why This Matters
AI-generated code is scaling fast; math-based proof layers could be its safety net.
A wave of startups including &Truth ($70M raised) and Harmonic ($295M) are using AI to automate formal verification—math-based software proofing once too costly for mainstream use—amid growing concerns over AI-generated code quality.
Stanford researcher Chuyue Sun and colleagues used an AI tool to complete a formal verification project in under half a day for less than $500—work that previously took three experts five months. That result helped validate a nascent industry around AI-assisted formal verification, a decades-old discipline that uses mathematical proofs to confirm software behaves exactly as intended, catching bugs that even extensive testing misses.
Sun joined &Truth in August; the startup publicly launched this week with $70 million in funding and plans to eventually verify any programming language. One early demo verified encryption code in Signal. Rival Harmonic—cofounded by Robinhood CEO Vlad Tenev and backed by $295 million including Nvidia's VC arm—announced its AI agent Aristotle now supports C code and Verilog hardware designs, with Tensordyne and Nvidia evaluating the tech. Anthropic and startup Theorem also jointly announced last week that AI helped find bugs in open source software that trillions of conventional tests had missed, alongside a Claude add-on for verification workflows.
Despite the momentum, the field is still early. Formal verification depends on precise assumptions about how humans and hardware interact with software, and critics note it struggles with bugs rooted in user error or hardware failures. Adoption and pricing models remain undefined, and widespread deployment beyond high-stakes environments like NASA and Apple is far from guaranteed.