AI startups want formal verification to scale beyond critical software

What formal verification can catch

Software testing looks for defects by running programs through many scenarios. Formal verification takes a different route: engineers describe how a program should behave, then translate its code into mathematics that can be checked. That can expose unusual failures that ordinary tests miss, but the work has historically been slow and difficult to scale.

The method is already used in some high-stakes systems. Companies say formally verified software is in Boeing aircraft, Amazon servers and more than 2.5 billion active Apple devices. It is usually applied to safety-related code, where an exploited vulnerability could cause serious damage.

Byron Cook, distinguished scientist and vice president at Amazon Web Services, says verification has helped address customer security concerns about cloud services and allowed internal teams to fix serious bugs earlier.

But its use remains limited. Several midsize technology companies told WIRED they had formally checked, at most, one important feature of a product. They cited a shortage of verification engineers, costs that do not match the perceived risk, and concern that waiting weeks for a review could slow development.

The new wave of AI tools

&Truth has raised $70 million from investors and hopes eventually to verify software written in any language. Its competitor Harmonic, co-founded by Robinhood CEO Vlad Tenev, has raised $295 million. This week, Harmonic said its math-focused AI agent Aristotle can verify C programs and hardware designs written in Verilog. The company is testing the technology with potential customers, including chipmakers Tensordyne and Nvidia; Nvidia’s venture arm has also invested in the startup.

Last week, Anthropic and startup Theorem said they had used AI to find bugs in open-source software that had survived trillions of tests. They also introduced an add-on for Claude to help developers with verification. They did not disclose the cost of the initial project.

Startups are exploring different ways to bring the tools to customers: selling directly or working through intermediaries such as Anthropic. Their shared ambition is to use AI to automate much of the work of specifying expected behavior. A specification for a data table, for example, might say that sorting must preserve the same elements while changing only their order. The code then has to be translated into a form that mathematical tools such as Lean, Rocq and Isabelle can check; that step may not require AI.

The field also has established providers. Proofcraft says rising interest has brought a surge of inquiries from potential clients, with demand well beyond what it and competitors can handle. Meanwhile, open-source projects are trying AI verification too. The nonprofit Beneficial AI Foundation, funded by a grant from Anthropic, checked the same encryption code that Sun studied at Stanford this year. Michael Rosenberg, maintainer of the curve25519-dalek library, hopes reliable funding will emerge, but says he does not know how to achieve it and does not think open-source projects should rely on AI companies’ goodwill.

The gap between proof and confidence

The attraction is clear: formal verification could make software more reliable and reduce security risks. Earlier this year, Apple’s security team said formal verification found problems in its corecrypto encryption library that other methods could not detect. Apple also said it must add code cautiously so there is time to verify it.

But a proof only covers what its specification describes. Some specialists doubt verification can catch failures caused by user behavior or hardware breakdowns. Will Wilson, head of bug-finding startup Antithesis, calls formal verification a “trap” for people who love mathematics. Antithesis spent millions of dollars formally checking some cybersecurity tools, a process Wilson describes as “a hell of a hassle.” Its own tool still found additional bugs, including in software that some customers had already formally verified. Wilson says verification can offer some confidence, but only thorough, exhaustive testing can confirm it.

Vitalik Buterin, the Ethereum creator, wrote earlier this year that formal verification is not a panacea. Still, he and other supporters argue it could help defend against cyberattacks and large-scale failures caused by AI systems.

I think the missing piece is not whether AI can produce a proof, but whether the specification deserves the confidence that proof invites. Proofcraft’s leaders, June Andronik and Gerwin Klein, worry that AI-generated specifications could create unjustified trust in verification results. Andronik and Klein also say demand already exceeds the capacity of providers.

The commercial question remains unresolved. Two cybersecurity executives at large companies that have not formally verified any software said they were unsure automation would make the process worthwhile, though they could imagine paying major AI labs for AI-generated code that had been verified. The work also depends on people who know how to define the behavior being proved—and on someone paying for that effort.

Madan Musuvathi, after more than 20 years at Microsoft Research, left to found Truidic. He says the OpenAI hack of Hugging Face made him feel an urgent need to bring his research to market. His view is that AI could become extremely powerful in attackers’ hands, and verification could help make it safer.

The promise, then, is not proof that software cannot fail. It is a way to check more of the assumptions behind critical code, while the people building these systems still have to decide which assumptions—and which risks—are worth paying to examine.