AI Software Verification Startups Raise $365M to Mathematically Prove Bug-Free Code

AI Slashes Software Verification Time From Five Months to Half a Day

Stanford researcher Chuyue Sun and her team achieved a breakthrough that signals a paradigm shift in software development: an AI tool completed a formal verification engineering project in less than half a day for under $5001

1

. The same work took three highly skilled experts five months to complete manually. Sun's research demonstrated the technology's potential by using AI to verify part of the code that encrypts conversations in the messaging app Signal, awakening an obscure field of coding and mathematics known as formal verification.

For decades, developers have envisioned using math to prove software correctness and create bug-free code. This process requires engineers to write precise statements about their software's goals and convert code into formulas that can be validated—a long and laborious undertaking. While companies run sophisticated tests to identify flaws, they rarely invest in formal verification, which can catch even more erratic behavior that standard testing misses.

Generative AI Makes Formal Methods Practical

A wave of startups is now betting that generative AI will make formal software verification both practical and essential. Among them is &Truth, which Sun joined in August and publicly launched on Thursday1

1

. The Palo Alto-based startup has raised $70 million from investors and aims to eventually verify any programming language. Clark Barrett, a Stanford University professor and &Truth co-founder, explained the significance: "It is possible to do something that was not possible before. You've seen what has happened in mathematics—proving these massive open conjectures. We can apply the same formal methods to verifying software"2

2

.

Rival Harmonic, cofounded by Robinhood CEO Vlad Tenev and backed by $295 million in funding, announced this week that its math-focused AI agent Aristotle supports verifying software written in C and hardware designs in Verilog1

1

. The startup is evaluating the technology with potential users, including chipmakers Tensordyne and Nvidia, whose venture capital arm is one of its investors.

Cybersecurity Crisis Drives Urgent Need

The implications of AI's newfound mathematical skills extend well beyond academic research. Using similar techniques that allowed OpenAI's technology to solve the Navier-Stokes problem in less than a week—a mathematical puzzle that bedeviled humans for decades—Silicon Valley is building AI systems that aim to eliminate security vulnerabilities in computer software2

2

. Just as an AI system can prove a math problem, it can theoretically prove that a software application is bug-free.

This sweeping effort to guarantee software integrity is vitally important as the internet faces its biggest cybersecurity threat in decades. Now that leading AI systems can hack into computer software by identifying and exploiting flaws with stunning speed, the world needs AI-powered verification to remove these vulnerabilities before AI-driven cyberattacks exploit them. Ilya Sergey, &Truth's chief science officer, draws a parallel: "Bridges, buildings, they don't collapse because people did math before constructing them. Why don't we do the same for code? The technology to mathematically reason was all there, just difficult to scale"1

1

.

Major Tech Companies Already Deploy Verified Software

Boeing planes, Amazon servers, and more than 2.5 billion active Apple devices contain at least some formally verified software, according to company disclosures1

1

. The code in question is typically security-related, where vulnerabilities could cause serious harm if exploited. Byron Cook, a distinguished scientist and vice president at Amazon Web Services, says formal verification has eased customer concerns about cloud security and helped internal teams move faster by squashing big bugs early on.

Earlier this year, Apple's security team revealed that formal verification uncovered issues in its "corecrypto" library used for encryption that could not have been found any other way1

1

. Last week, Anthropic and verification startup Theorem jointly announced they used AI to assist in finding bugs in open source software that trillions of tests had failed to detect1

1

. They also introduced an add-on for Claude to help other developers with verification.

Skeptics Question Practical Limitations

Despite the momentum, several midsized tech companies tell WIRED they have typically verified only one key feature of their products, if any at all. They cite a lack of verification engineers, costs that outweigh potential risks, and concerns that waiting weeks for code to be formally verified could slow innovation1

1

.

Will Wilson, who runs bug-hunting AI software startup Antithesis, calls formal verification "a trap" for math nerds like himself. Antithesis spent millions of dollars to formally verify some of its cybersecurity defenses—a process Wilson describes as a "pain in the ass"—yet the startup still uncovered additional errors using its own tool1

1

. 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 warns.

Vitalik Buterin, the engineer known for creating Ethereum cryptocurrency, wrote in a blog post earlier this year that "formal verification is not a panacea." But he and other proponents still believe it will be an important defense against AI systems launching cyberattacks and wreaking havoc1

1

.

Lean Programming Language Emerges as Key Tool

Much like Silicon Valley startups Axiom and Logical Intelligence, along with leading AI labs like Anthropic and OpenAI, &Truth hopes to eradicate computer bugs using a specialized computer programming language called Lean2

2

. This is the same tool that allows AI technologies to solve million-dollar mathematics problems. The technology is still in the prototyping stage, and while demand is high, it remains unclear how much customers are willing to pay and how they prefer to adopt the technology. Formal verification relies on making assumptions about how computers and people interact with software, and some experts remain skeptical about its ability to catch bugs stemming from user error and hardware breakdowns1

1

.