AI Could Make Mathematical Software Verification Practical
Startups are betting that generative AI will make formal verification, the mathematical proof that software is free of bugs, cheaper and more widely used. Experts remain divided on whether it can move beyond the most critical systems.
Stanford University researcher Chuyue Sun and fellow computer scientists built an AI tool that finished an engineering project in under half a day for less than $500. Three highly skilled experts had needed five months to do the same work by hand. These early results are drawing attention to formal verification, a niche field of coding and mathematics in which software is proven mathematically to behave as intended.
The process has traditionally been long and laborious: engineers must write precise statements about what the software should do and convert the code into formulas that can be checked. Companies run sophisticated tests, but rarely pay for formal verification, even though it can catch more erratic behavior.
A race among startups
A wave of startups now hopes generative AI will make it practical. Sun joined &Truth in August; the company launched publicly on Thursday and has raised $70 million. Her research used AI to verify part of the code that encrypts conversations in the messaging app Signal. Rival Harmonic, cofounded by Robinhood CEO Vlad Tenev and funded with $295 million, said its AI agent Aristotle can verify software written in C and hardware designs in Verilog. Potential users, including Nvidia and Tensordyne, are evaluating it. Last week Anthropic and the startup Theorem announced they had used AI to help find bugs in open source software that trillions of tests had missed.
Doubts and limits
The technology is still at the prototype stage, and it is unclear how much customers will pay. Some experts doubt it can catch bugs caused by user error or hardware failure. Will Wilson, who runs Antithesis, calls formal verification “a trap” and says only exhaustive testing can confirm assurance. Vitalik Buterin has also written that it is not a panacea.
Boeing planes, Amazon servers and Apple devices already contain some formally verified software. Midsized companies typically verify only one key feature, citing a shortage of specialists, costs, and the risk of slowing innovation. Proofcraft executives warn that AI-generated specifications could inspire “unjustified trust” in results.
