Stanford AI tool verifies part of Signal's code in half a day for under $500, versus five months of expert work

Formal verification, the mathematical proof that a program does exactly what it is supposed to do, has for decades been the preserve of enthusiasts and the most critical systems. Now generative AI is trying to turn it into an ordinary tool. Stanford researcher Chuyue Sun and her colleagues showed in a recent paper that their AI tool completed an engineering project in less than half a day for under $500. Three highly qualified experts had spent five months on the same work. The project covered part of the code that encrypts conversations in the Signal messenger.

Why the math suddenly got cheaper

Classical verification is hard for two reasons. Engineers must state precisely what they want from the program, and then translate the code into formulas that can be checked. Companies already run elaborate tests, but they rarely spend money on formal verification, even though it catches stranger failures.

New startups are betting on automating the first step. The AI is supposed to write specifications: for sorting a table, for example, they require that the set of elements stays the same before and after, with only the order changing. The next step, translating code into the format for the Lean, Rocq and Isabelle proof systems, can be done without AI.

Sun moved to &Truth in August, and the company launched publicly on Thursday. The startup raised $70 million and wants to eventually verify code in any language. &Truth chief scientist Ilya Sergey compares it to construction: bridges and buildings don't collapse because they are calculated in advance, and the technology for this kind of reasoning about code has existed but scaled poorly.

Who else is working on this market

Competitor Harmonic, co-founded by Robinhood chief Vlad Tenev, has raised $295 million. This week the company announced that its AI math agent Aristotle can verify software in C and hardware descriptions in Verilog. Potential customers are evaluating the technology, including chipmaker Tensordyne and Nvidia, whose venture fund is among Harmonic's investors.

A week earlier, Anthropic and the startup Theorem reported that they had used AI to find bugs in open-source software that trillions of tests had missed. They also released an add-on for Claude to help developers with verification. The cost of the first project was not disclosed. Madan Musuvathi, who left Microsoft Research after more than 20 years, founded Truidic: he says AI is very powerful in the hands of attackers, and verification can make AI systems safe.

The Beneficial AI Foundation, using an Anthropic grant, verified the same cryptographic code as Sun this year. Michael Rosenberg, maintainer of the curve25519-dalek library, hopes for sustainable funding but does not know where it will come from, and considers it wrong to rely on the goodwill of AI companies.

Where the skepticism and limits lie

Verification is already in Boeing aircraft, Amazon servers and more than 2.5 billion active Apple devices, but it is usually security-related code. Byron Cook of AWS says the method eased some cloud customers' concerns and sped up internal teams. On the other hand, several mid-sized companies told WIRED they had verified at most one key function. The reasons: a shortage of specialists, costs that exceed the possible risks, and fear that weeks of waiting would slow product releases. Two cybersecurity executives at large companies that have not formally verified code are not sure automation will change the calculation, but are ready to pay major AI labs for "verified" generated code.

The technology is still at the prototype stage. It is unclear how much customers are willing to pay and how they want to adopt it: directly or through intermediaries such as Anthropic. The method relies on assumptions about how computers and people interact with software, so some experts doubt it will catch user errors and hardware failures.

Will Wilson, head of the startup Antithesis, which hunts for bugs with AI, calls formal verification a "trap" for mathematicians like him. The company spent millions of dollars verifying part of its defenses, calling the process painful, and still found additional bugs with its own tool. Antithesis has also found bugs in customers' software that they had already verified. In his view, formal verification gives some confidence, but only exhaustive testing can confirm it. Vitalik Buterin has also written in a blog that it is not a panacea.

Another caveat concerns the specifications themselves. Proofcraft founders June Andronick and Gerwin Klein say interest exceeds their capacity and that of their competitors, but they fear "undue trust" in results with AI-written specifications. The practical takeaway for teams: AI makes verification cheap enough to try on critical modules such as cryptography, but it does not promise to replace tests.