&Truth, a startup that aims to verify code in any programming language, launched publicly on Thursday with $70 million of funding.
Its approach rests on formal verification, which converts code into mathematical statements that can be checked, proving the software is free of certain bugs.
Chuyue Sun, a Stanford computer scientist who joined the company in August, used an AI tool to verify part of the encryption code behind the Signal messaging app in under half a day for less than $500, according to Wired.
A project of that kind took three highly skilled human experts five months.
Formal verification has existed for decades but has been too slow and expensive for most companies to adopt widely.
"Bridges, buildings, they don't collapse because people did math before constructing them," said Ilya Sergey, &Truth's chief science officer.
"Why don't we do the same for code?" he said.
Crowded field
Harmonic, cofounded by Robinhood chief executive Vlad Tenev and backed by $295 million in funding, said this week its AI agent Aristotle now supports verifying code written in C, a widely used programming language.
The tool also covers hardware designs written in Verilog, a language used to describe computer chips, and is being tested with chipmakers Tensordyne and Nvidia.
Anthropic and the startup Theorem said last week they had used AI to find bugs in open source software that had evaded trillions of earlier tests.
The two companies also launched a verification add-on for Claude, Anthropic's AI assistant.
Limits remain
Formal verification already underpins parts of Boeing's planes, Amazon's servers and more than 2.5 billion active Apple devices.
Most midsized technology firms say they verify at most one key feature, citing cost and a shortage of engineers.
Will Wilson, founder of Antithesis, whose company has formally verified some of its own cybersecurity defences, called the process "a pain in the ass".
He said it had still missed bugs that his own testing tools caught.
