Stanford researcher Chuyue Sun and colleagues developed an AI tool that completed an engineering project in under half a day for less than $500, a stark contrast to the five months required for three skilled experts to perform the same work manually. This early result highlights the potential of formal verification, an obscure field of coding and mathematics that aims to mathematically prove software is bug-free. The process traditionally requires engineers to write precise statements about software goals and convert code into verifiable formulas, a process companies rarely fund despite running sophisticated flaw-finding tests.
Sun joined the startup &Truth in August, which publicly launched on Thursday, demonstrating the technology's capability by using AI to verify part of the code that encrypts conversations in the messaging app Signal. Ilya Sergey, &Truth’s chief science officer, stated, “Bridges, buildings, they don’t collapse because people did math before constructing them.” &Truth has raised $70 million and intends to eventually verify any programming language.
Rival Harmonic, cofounded by Robinhood CEO Vlad Tenev and backed by $295 million, announced that its math-focused AI agent Aristotle supports verifying software written in C and hardware designs in Verilog, and it is evaluating the technology with potential users including chipmakers Tensordyne and Nvidia. Furthermore, Anthropic and the verification startup Theorem jointly announced using AI to assist in finding bugs in open source software that trillions of tests had failed to detect, and they introduced an add-on for Claude to aid developers with verification. While Core Security, Boeing planes, Amazon servers, and over 2.5 billion active Apple devices contain at least some formally verified software, the technology remains in the prototyping stage, and experts question its ability to catch bugs stemming from user error and hardware breakdowns.
Will Wilson, who runs the bug-hunting AI software startup Antithesis, called formal verification “a trap” for math nerds, noting that even after spending millions to formally verify cybersecurity defenses, Antithesis still uncovered additional errors using its own tool.
