AI Verified Part of Signal's Code with Math in Half a Day for $500, Versus Five Months by Hand

Stanford researcher Chuyue Sun and her colleagues built an AI tool that completed an engineering project in under half a day for less than $500: it verified part of the code that encrypts conversations in the Signal messenger. Three highly qualified specialists spent five months doing the same work by hand. The check was not an ordinary one but a formal one. Instead of running the program through thousands of tests, the engineers mathematically prove that it behaves as intended. The idea is old, but until now it has been too expensive and too slow. Now startups with hundreds of millions of dollars and major AI labs are betting on it.

Why math instead of tests

Conventional testing shows that a program did not break in the cases it was fed. Formal verification proves that it will not break in any case within a described class. Engineers write precise statements about what the program is meant to do, then translate the code into formulas that dedicated systems check. Such systems include Lean, Rocq and Isabelle.

But the work is heavy. Specifications have to be written very carefully. A simple example: a function that sorts a table must return the same elements it received, just in a different order. That is obvious to a human, but a mathematical system needs it spelled out strictly.

That is why the method is used where the cost of a mistake is high. According to company disclosures, formally verified code is present in Boeing aircraft, on Amazon servers and in more than 2.5 billion active Apple devices. This is usually security-related code. Byron Cook of Amazon Web Services says verification answered customers' questions about cloud security and sped up internal teams: major bugs were caught early.

Who is betting on AI, and how

Startups want to automate the most tedious part: writing the description of how the program should behave. The remaining steps, possibly even without AI, then translate the code into a format for the mathematical systems.

• &Truth. Raised $70M. Sun joined in August, and the public launch took place on Thursday.

The goal is eventually to verify code in any programming language. Scientific director Ilya Sergey compares the approach to construction: bridges and buildings do not collapse because they were calculated before being built, so why not do the same with code. • **Harmonic.

** Co-founded by Robinhood chief Vlad Tenev; has raised $295M. This week the company announced that its math AI agent Aristotle can verify programs in C and chip descriptions in Verilog. Potential customers are evaluating the technology, including chipmakers Tensordyne and Nvidia; Nvidia's venture arm is one of the investors.

• Anthropic and Theorem. A week ago they reported that they used AI to find bugs in open-source software that trillions of tests had not caught. They also released an add-on for Claude that helps developers with verification.

The cost of the first project was not disclosed. • Truidic. Founded by Madan Musuvathi, who left Microsoft Research after more than 20 years.

In his view, AI in the hands of attackers is very powerful, and verification can make AI safe. • Proofcraft. Has long worked on classical verification.

Its leaders June Andronick and Gerwin Klein say the flow of requests exceeds the capacity of both their own team and their competitors.

Open projects are trying the method too. The nonprofit Beneficial AI Foundation, on an Anthropic grant, verified the same encryption code as Sun this year. Michael Rosenberg, one of the maintainers of the curve25519-dalek library, hopes for permanent funding for this kind of work, but does not know where it will come from and does not want to rely on the goodwill of AI companies.

Where the method hits a ceiling

For now, the technology is at the prototype stage. It is unclear how much customers are willing to pay and in what form they want to receive the product: directly or through intermediaries such as Anthropic. Several mid-sized tech companies told Wired that they had verified at most one core product function, and sometimes none. The reasons: a shortage of verification engineers, a cost higher than the potential risk, and the fear that weeks of waiting for verification would slow down update releases. Even Apple has to add new code to its corecrypto encryption library cautiously, so that it can keep up with verifying it.

There are also objections of principle. A proof relies on assumptions about how computers and people interact with the program. It may not catch user errors or hardware failures.

Will Wilson, head of the AI bug-hunting startup Antithesis, calls formal verification a "trap" for math lovers like himself. His company spent millions verifying part of its own security, calling the process a "pain in the ass." But the company's own tool still found additional bugs in it, as well as bugs in customers' software that those customers had already formally verified.

Wilson's conclusion: verification gives some confidence, but only exhaustive testing can confirm it. Vitalik Buterin also wrote in his blog that formal verification is not a panacea, although he considers it an important defense against AI-assisted cyberattacks.

Andronick and Klein see a separate risk: if AI wrote the problem description, it creates "unwarranted trust" in the result. A proof is only as correct as the description of what counts as correct.

The practical takeaway for engineers: AI sharply lowers the cost of the most expensive stage, but both the specifications themselves and the work will still have to be checked with tests. Two companies that do not formally verify their code would be willing to pay AI labs for "verified" code generated by AI. If that works, formal verification will move beyond NASA and Apple.