AI Brings Formal Verification to Real-World Software Code

By Marcus Bennett

Stanford researcher Chuyue Sun reported in a recent paper that an AI tool developed by her and fellow computer scientists completed an engineering project in less than half a day for less than $500. Three highly skilled experts needed five months to perform the same work manually.

Sun’s paper was among the early results drawing renewed attention to formal verification, an obscure field joining coding and mathematics. The stakes are operational rather than academic: startups want proof tools that scale, while customers want fewer failures and exploitable vulnerabilities.

For decades, developers have envisioned using mathematics to prove their software bug-free, WIRED reported. The long, labor-intensive process requires engineers to write precise statements about software goals and translate code into formulas that mathematical tools can validate.

What does AI add to formal verification?

Formal verification is a software-testing process that uses mathematical proofs to show that code meets stated behavioral requirements. Conventional test suites identify as many flaws as possible, but companies rarely fund formal verification. WIRED’s reporting says the method can catch even more erratic behavior.

Sun applied AI to part of the code that encrypts conversations in Signal. Her Stanford research demonstrated that AI could complete a formal-verification task in less than half a day for less than $500, compared with five months of manual expert work.

Ilya Sergey, &Truth’s chief science officer, framed the goal: “Bridges, buildings, they don’t collapse because people did math before constructing them,” he said. “Why don’t we do the same for code? The technology to mathematically reason was all there, just difficult to scale.”

Can startups scale formal verification?

• &Truth: Sun joined the company in August, and it publicly launched on Thursday. The startup raised $70 million and aims eventually to verify any programming language.
• Harmonic: Robinhood CEO Vlad Tenev co-founded the rival, which has received $295 million. This week, Harmonic said its mathematics-focused AI agent, Aristotle, supports verifying software written in C and hardware designs in Verilog.
• Anthropic and Theorem: The companies said last week that they used AI to assist in finding open source bugs that trillions of tests had failed to detect. They introduced a verification add-on for Claude and did not disclose the initial project’s costs.

Harmonic is evaluating Aristotle with potential users, including chipmaker Tensordyne and Nvidia. Nvidia’s venture capital arm is an investor in Harmonic.

A wave of companies, including &Truth, Harmonic, Anthropic and Theorem, is betting that generative AI will make formal verification both practical and essential. The larger promise is software that runs more reliably with fewer security problems. Its unresolved role is whether AI can move verification beyond critical systems at organizations such as NASA and Apple into widespread development.

How much formally verified software is in use?

Company disclosures show that Boeing planes, Amazon servers, and more than 2.5 billion active Apple devices contain at least some formally verified software. The code usually addresses security functions, where an exploited vulnerability could cause serious harm.

Byron Cook, a distinguished scientist and vice president at Amazon Web Services, said formal verification has eased customer concerns about cloud security. He also said it has helped internal teams move faster by removing major bugs early.

Several midsized technology companies told WIRED that they typically verify one key feature, if any. They cited a shortage of verification engineers, costs that outweigh the perceived risks, and weeks-long waits that could slow product innovation.

Earlier this year, Apple’s security team said some issues found in its “corecrypto” encryption library could not have been found any other way. Apple must remain “conservative” when adding code to corecrypto, however, so review can keep pace with each change.

Two cybersecurity executives at major companies that have not formally verified any code told WIRED they remain unsure whether automation will make the process worthwhile. Both said they could imagine paying major AI labs for “verified” AI-generated code.

Why do some engineers distrust formal verification?

Will Wilson, who runs bug-hunting AI startup Antithesis, calls formal verification “a trap” for math nerds like himself. Antithesis spent millions of dollars formally verifying some of its cybersecurity defenses, a process Wilson describes as a “pain in the ass.”

The startup still uncovered additional errors with its own tool. Antithesis has also found bugs in software that several customers had formally verified. “It can give you some assurance, but only robust exhaustive testing can prove your assurance is true,” Wilson said.

Formal verification depends on assumptions about how computers and people interact with software. Experts cited in WIRED’s reporting doubt that it can catch every bug caused by user error or hardware breakdowns.

Vitalik Buterin, the engineer who created the Ethereum cryptocurrency, wrote earlier this year that “formal verification is not a panacea.” He and other proponents still consider it an important defense against AI systems launching cyberattacks and causing widespread harm.

Can AI automate formal proof work?

WIRED reported that developers of open source software, which forms the bedrock of many applications, are increasingly experimenting with AI-aided verification. The nonprofit Beneficial AI Foundation used an Anthropic grant to validate the same encryption code this year that Sun validated at Stanford.

Michael Rosenberg, a maintainer of the curve25519-dalek library, wants sustainable funding for continuing verification. “I have no ideas as to how that’s going to happen, though, and we certainly shouldn’t rely on the goodwill of the AI companies,” he said.

The verification startups remain undecided whether to sell directly to customers or through intermediaries such as Anthropic. Their general plan uses AI to automate much of the work required to define how a program should behave.

That definition starts with a specification, or precise statement of required behavior. One example requires a data table to contain the same items before and after sorting, but in a different order.

Further automation, which may not involve AI, would translate code into a format that the mathematical tools Lean, Rocq and Isabelle can check. In that workflow, AI helps generate behavioral requirements before mathematical software checks the resulting code.

Madan Musuvathi left Microsoft Research after more than 20 years to found Truidic. Following incidents such as the OpenAI hack of Hugging Face, he saw an urgent need to commercialize his research. “AI in the hands of attackers can be extremely powerful,” Musuvathi said, but verification can “make AI safe and secure for everyone, everywhere.”

Proofcraft, one of the few companies offering traditional verification for a long time, reports a surge in inquiries. CEO June Andronick and chief scientist Gerwin Klein say demand easily exceeds what they and their competitors can provide.

Both worry that AI-generated specifications could create “unjustified trust” in the results. They also want to preserve the appeal of verification work. Klein called it “pretty addictive, like a puzzle game,” and said success could let him spend more time solving problems.

What will determine adoption?

WIRED described the technology as still in its prototyping stage despite strong demand. Potential customers have not established how much they will pay or which deployment model they prefer.

The next test is practical rather than mathematical. Startups must show that AI-generated specifications do not create “unjustified trust,” while customers must decide whether formal proof justifies the cost and weeks-long review delays.

That reckoning will determine whether Sun’s less-than-half-day, sub-$500 result becomes routine in software development or remains concentrated in security-critical code, hardware designs and systems operated by organizations such as NASA and Apple.