&Truth, Harmonic and rivals bet AI can make formal code verification practical

Wired reports that a small, obscure field called formal verification is being woken up by generative AI. Formal verification means using math to prove that software is free of bugs. It has long been slow and laborious: engineers must write precise statements about what the software is meant to do and convert the code into formulas that can be validated. Companies already run sophisticated tests, and they rarely pay for verification, even though it can catch more erratic behaviour.

The lead result comes from Stanford researcher Chuyue Sun and her fellow computer scientists. They built an AI tool that completed an engineering project in less than half a day for under $500. Three highly skilled experts had needed five months to do the same work manually. Sun reported the figures in a recent paper. Her research used AI to verify part of the code that encrypts conversations in the messaging app Signal. Sun joined the startup &Truth in August, and &Truth publicly launched on Thursday. It has raised $70 million from investors and aims to eventually verify any programming language. Its chief science officer, Ilya Sergey, argues that bridges and buildings don't collapse because people did math before constructing them, and asks why the same isn't done for code. In his words, the technology to reason mathematically was all there, just difficult to scale.

&Truth is not alone. Rival Harmonic, cofounded by Robinhood CEO Vlad Tenev, has received $295 million in funding. This week it announced that its math-focused AI agent Aristotle supports verifying software written in C and hardware designs in Verilog. Harmonic is evaluating the technology with potential users including chipmakers Tensordyne and Nvidia, whose venture capital arm is one of Harmonic's investors. Last week Anthropic and the verification startup Theorem jointly announced they had used AI to help find bugs in open source software that trillions of tests had failed to detect. They also introduced an add-on for Claude to help other developers with verification. Costs of that initial project were not disclosed. Another newcomer is Madan Musuvathi, who left Microsoft Research after more than 20 years to found Truidic. After incidents like the OpenAI hack of Hugging Face, he felt there was an urgent need to commercialize his studies. He says AI in the hands of attackers can be extremely powerful, but verification can make AI safe and secure for everyone, everywhere.

The startups' general plan is to use AI to automate much of the work of defining how a program should behave. An example specification: a data table must contain the same items before and after sorting, just in a different order. Further automation, which may not involve AI, then translates the code into a format that math tools such as Lean, Rocq and Isabelle can use to check whether it works as intended.

Formal verification is not new in production. Boeing planes, Amazon servers and more than 2.5 billion active Apple devices contain at least some formally verified software, according to company disclosures. The code is typically security-related. Byron Cook, a distinguished scientist and vice president at Amazon Web Services, says it has eased customer concerns about cloud security and helped internal teams move faster by squashing big bugs early. Earlier this year Apple's security team said some issues that verification uncovered in its corecrypto encryption library could not have been found any other way, though the company added that it has to be conservative when adding new code to corecrypto so that it can keep pace with reviewing it.

Several midsized tech companies told Wired they have typically verified only one key feature of their products, if any. They cite a lack of verification engineers, costs that outweigh the potential risks, and concerns that waiting weeks for verification could slow innovation. Two cybersecurity executives at major companies that haven't formally verified any code, who weren't authorized to speak publicly, aren't sure automation will make it worthwhile, but could imagine paying major AI labs for 'verified' AI-generated code.

The critics are pointed. Will Wilson, who runs the bug-hunting AI startup Antithesis, calls formal verification 'a trap' for math nerds like himself. Antithesis spent millions of dollars verifying some of its cybersecurity defenses, a process he calls a 'pain in the ass'. The startup still found additional errors with its own tool, and has found bugs in software that several of its customers had formally verified. Wilson says verification can give some assurance, but only robust exhaustive testing can prove the assurance is true. Vitalik Buterin wrote in a blog post earlier this year that 'formal verification is not a panacea', though he and other proponents still expect it to be an important defense against AI-launched cyberattacks.

Open source projects are experimenting too. The nonprofit Beneficial AI Foundation used a grant from Anthropic to validate the same encryption code as Sun did at Stanford. Michael Rosenberg, a maintainer of the library known as curve25519-dalek, hopes sustainable funding emerges for ongoing verification, but says he has no ideas how that will happen and that nobody should rely on the goodwill of AI companies. Proofcraft, one of the few firms that has long offered traditional verification, reports a flood of inquiries; CEO June Andronick and chief scientist Gerwin Klein say interest easily outpaces what they and their competition can provide. Both worry that AI-generated specifications could inspire 'unjustified trust' in results. Klein calls the work 'pretty addictive, like a puzzle game'.

Wired's bottom line: the promise is software that runs more reliably with fewer security headaches, but whether AI can take verification beyond the most critical systems at organizations like NASA and Apple into widespread use remains an open question.

Key facts

Stanford researcher Chuyue Sun and colleagues built an AI tool that finished an engineering project in under half a day for under $500; three experts had needed five months doing it manually.
&Truth publicly launched on Thursday with $70 million raised; Harmonic (backed by $295 million) says its Aristotle agent now verifies C software and Verilog hardware designs.
Anthropic and Theorem said last week that AI-assisted work found open source bugs that trillions of tests had missed, and introduced a Claude add-on for verification.
Boeing planes, Amazon servers and more than 2.5 billion active Apple devices contain at least some formally verified software, per company disclosures, but several midsized firms verify at most one key feature.
The technology is still at the prototyping stage; Antithesis's Will Wilson calls verification 'a trap' and Proofcraft warns of 'unjustified trust' in AI-generated specifications.

Why it matters

Proving code correct with math has existed for decades but stayed confined to the most critical systems, because writing the specifications and proofs is slow and costly. If the Stanford figure holds up (under half a day and under $500 versus five months for three experts), the economics change. Startups are now betting that AI will make verification both practical and essential, partly as a defense against AI-driven cyberattacks, which is the argument Musuvathi and Buterin's camp make.

Who it affects

Software and chip teams working on security-sensitive code are the first audience: Harmonic is evaluating Aristotle with Tensordyne and Nvidia, and Anthropic's Claude add-on targets other developers. Open source maintainers such as those of curve25519-dalek are experimenting, and worry about who pays for ongoing work. Midsized companies, which verify at most one key feature, are the market the startups would need to win. Established verification firms such as Proofcraft report demand outrunning supply.

How to use it

The tools are early. Harmonic's Aristotle supports verifying C software and Verilog hardware designs and is being evaluated with potential users. Anthropic and Theorem introduced an add-on for Claude to help developers with verification. The general method is to have AI draft the specification of how a program should behave, then translate the code into a format that tools like Lean, Rocq and Isabelle can check. No product pricing is given, and some startups are unsure whether to sell directly or through intermediaries like Anthropic. Two security executives said they could imagine paying major AI labs for 'verified' AI-generated code.

How solid is it

The cost and time comparison comes from Sun's own recent paper, as reported by Wired; the article does not describe which project was involved. The Anthropic and Theorem bug-finding result is an announcement, and its costs were not disclosed. Claims about Boeing, Amazon and Apple come from company disclosures. The article itself says the technology is still in the prototyping stage, and that it is unclear how much customers will pay and how they prefer to adopt it. The press source is a single Wired feature.

Risks and caveats

Formal verification rests on assumptions about how computers and people interact with software, and some experts doubt it can catch bugs from user error or hardware breakdowns. Wilson's Antithesis spent millions on verification and still found further errors, and has found bugs in software that customers had formally verified. Buterin says it is not a panacea. Proofcraft's Andronick and Klein worry that AI-generated specifications could inspire 'unjustified trust'. Costs, a shortage of verification engineers and fear that weeks of waiting would slow innovation keep many companies away, and open source maintainers have no clear funding path. Apple said it must stay conservative about adding code to corecrypto so it can keep pace with reviewing it.

“Bridges, buildings, they don’t collapse, because people did math before constructing them”

— Ilya Sergey, &Truth’s chief science officer