Software verification uses mathematics to check whether code behaves as intended. New AI tools may make that work faster and less expensive, but wider adoption will depend on whether the results are useful, affordable and trusted.
AI could lower the cost of proving code
Formal verification has long promised stronger guarantees than ordinary software testing. Engineers describe what a program should do, then translate its code into formulas that mathematical tools can examine. The process can reveal unusual behavior that standard tests miss, but it has traditionally taken substantial time and specialist effort.
Research by Stanford computer scientist Chuyue Sun and colleagues offered an early sign that AI could change the economics. Their tool completed an engineering project in less than half a day for under $500; three highly skilled experts had spent five months doing the same work manually. Sun also used AI to verify part of the code that encrypts conversations in Signal.
That kind of speedup is attracting companies that hope to make verification more accessible. &Truth, which Sun joined in August and publicly launched on Thursday, has raised $70 million and aims to support any programming language over time. Harmonic, cofounded by Robinhood CEO Vlad Tenev, has received $295 million in funding. Its math-focused AI agent Aristotle supports verification for software written in C and hardware designs in Verilog.
What the verification process checks
The approach starts by defining expected behavior precisely. For a data table, for example, a requirement might say that sorting can change the order of items but must preserve the items themselves. AI could help create these specifications, while other automation translates them into a form that proof tools such as Lean, Rocq, and Isabelle can check.
The goal is to verify that a program satisfies the requirements it was given. That is a valuable check, especially for security-sensitive code, but it depends on the requirements being right and complete. Formal verification does not remove the need to decide what the software is meant to do.
That limitation matters because software operates in the real world. The method relies on assumptions about how people and computers interact with a program. Some experts question whether it can catch problems caused by user mistakes or hardware failures.
Adoption depends on time, cost and trust
Formal verification already appears in some critical systems. Company disclosures indicate that Boeing planes, Amazon servers, and more than 2.5 billion active Apple devices contain at least some formally verified software. The verified code is typically related to security, where a vulnerability could cause serious harm if exploited.
Still, use is limited at many companies. Several midsized technology firms told WIRED they had verified only one key product feature, if any. They pointed to the shortage of verification engineers, costs that can exceed the perceived risk, and the possibility that waiting weeks for a review could slow development.
Apple has said that formal verification found issues in its corecrypto encryption library that could not have been discovered another way. The company also said it must be conservative about adding code so its team can keep up with reviews. Automation may ease that burden, but potential customers have not settled on how they want to buy or use the tools.
AI developers are also weighing whether to sell verification directly or offer it through other companies. Executives at two major companies that have not formally verified code said they were unsure whether automation would make the process worthwhile, though they could imagine paying AI labs for verified AI-generated code.
A useful safeguard, with limits
AI-assisted verification has also drawn attention from open source maintainers. The Beneficial AI Foundation used an Anthropic grant to validate the same encryption code that Sun studied. Michael Rosenberg, maintainer of curve25519-dalek, said ongoing work needs sustainable funding and should not depend on AI companies acting out of goodwill.
Other recent efforts include a collaboration between Anthropic and Theorem, which used AI to help find bugs in open source software that trillions of tests had not detected. They also introduced a Claude add-on to help developers with verification. The cost of that initial project was not disclosed.
There is no consensus that mathematical verification can replace testing. Will Wilson of Antithesis describes the process as a “pain in the ass”: his company spent millions verifying some cybersecurity defenses and later found additional errors with its own tool. Antithesis has also found bugs in software its customers had formally verified. Wilson argues that verification offers some assurance, while robust exhaustive testing is needed to establish whether that assurance holds.
For now, AI could help extend a technique already used in selected high-stakes systems, while reducing the expert labor involved. Whether it reaches routine software development will depend on practical questions of cost, workflow and confidence in the specifications and proofs. As Vitalik Buterin put it, “formal verification is not a panacea.”