A Stanford-developed AI tool completed an engineering verification project in less than half a day for under $500, work that previously required three highly skilled experts and five months to finish manually. Researcher Chuyue Sun reported the dramatic cost and time reduction in a recent paper, marking one of the earliest demonstrations that generative AI can make formal verification—a decades-old mathematical approach to proving software is bug-free—both practical and affordable. The findings are reviving interest in a field that companies have long considered too expensive and time-consuming to use beyond their most critical systems.
Several startups are now racing to commercialize AI-powered verification tools. &Truth, which Sun joined in August and launched publicly on Thursday, has raised $70 million from investors and aims to verify software in any programming language. Rival Harmonic, cofounded by Robinhood CEO Vlad Tenev, announced this week that its AI agent Aristotle can verify software written in C and hardware designs in Verilog after securing $295 million in funding. The company is testing the technology with chipmakers Tensordyne and Nvidia, whose venture arm is among its investors. Last week, Anthropic and verification startup Theorem revealed they used AI to find bugs in open source software that trillions of tests had missed, and introduced an add-on for Claude to help developers with verification. Boeing planes, Amazon servers, and more than 2.5 billion active Apple devices already contain at least some formally verified software, according to company disclosures, though the code in question is typically limited to security-related features where vulnerabilities could cause serious harm if exploited.
According to Ilya Sergey, &Truth's chief science officer, "Bridges, buildings, they don't collapse because people did math before constructing them. Why don't we do the same for code?" The report notes that several midsized tech companies typically verify only one key feature of their products, if any at all, citing a shortage of verification engineers and concerns that waiting weeks for code to be formally verified could slow innovation. Earlier this year, Apple's security team stated that some issues formal verification uncovered in its "corecrypto" library, used for encryption, couldn't have been found any other way. But the company added that it must be "conservative" when adding new code to corecrypto to ensure it can keep pace with reviewing it. Will Wilson, who runs bug-hunting AI software startup Antithesis, calls formal verification "a trap" for math nerds, noting his company spent millions of dollars to formally verify some of its cybersecurity defenses yet still found additional errors using its own tool.
The startups plan to use AI to automate much of the work involved in defining how a program is supposed to behave, then translate code into a format that mathematical tools like Lean, Rocq, and Isabelle can use to check whether it functions as intended. Madan Musuvathi, who left Microsoft Research after more than 20 years to found startup Truidic, says AI in the hands of attackers can be extremely powerful, but verification can make AI safe and secure for everyone. Proofcraft, one of the few companies that has long offered traditional verification, reports that growing excitement about the process is translating into a flood of inquiries from potential customers, with interest easily outpacing what the company and its competition can provide. However, Proofcraft's CEO June Andronick and chief scientist Gerwin Klein worry that AI-generated specifications could inspire "unjustified trust" in the results. Two cybersecurity executives at major companies that haven't formally verified any code say they aren't sure whether automation will make it worthwhile, though they could imagine paying major AI labs for "verified" AI-generated code. Companies still face hard choices about whether to adopt formal verification broadly or reserve it for their most sensitive systems, and the balance between speed and mathematical certainty will likely define which organizations gain competitive advantage as AI-powered attacks grow more sophisticated.