In September, OpenAI announced that its new artificial intelligence (AI) technology needed less than a week to solve the Navier-Stokes problem, a mathematical puzzle that bedevilled the world’s smartest humans for decades. In the weeks that followed, the company released a deluge of additional findings that stunned leading mathematicians and raised new questions about the future of an academic field that has long been viewed as the pinnacle of human achievement.
But the implications of AI’s newfound mathematical skills extend well beyond academic research. Using similar techniques, Silicon Valley is now building AI systems that aim to eliminate the dangerous flaws, or “bugs,” in the world’s computer software. Just as an AI system can prove a math problem, it can prove that a software application is bug-free – at least in theory.
This sweeping effort to guarantee the integrity of computer software, which scientists call “software verification,” is vitally important as the Internet faces its biggest cybersecurity threat in decades. Now that the leading AI systems can hack into computer software, by identifying and exploiting its flaws with stunning speed, the world needs a new breed of AI that can remove these flaws.
&Truth, a new startup based in Palo Alto, California, is among the many companies working to build this kind of technology. Much like the Silicon Valley startups Axiom and Logical Intelligence and leading AI labs like Anthropic and OpenAI, &Truth hopes to verify the world’s software using a specialised computer programming language called Lean, the same tool that allows AI technologies to solve million-dollar math problems.
“It is possible to do something that was not possible before,” said Clark Barrett, a Stanford University professor who is among the founders of &Truth and its co-chief executive. “You’ve seen what has happened in mathematics – proving these massive open conjectures. We can apply the same formal methods to verifying software.”
Software bugs arise when applications do things they were not designed to do. An application might store information in the wrong database or write too much information into system memory, so that it spills into the wrong memory register and corrupts other data. Malicious attackers can use these bugs to hack their way into the application.
Software verification is an effort to prevent such mistakes at a logical level. The aim is to formally prove that an application behaves only as it was designed to behave, much in the way that mathematicians prove math problems – one logical step at a time.
Experienced engineers can verify software by hand, but this requires years of work. Now, companies like &Truth are working to build AI systems that can verify software in a matter of hours or days, which would finally provide a practical way of ensuring the integrity of computer software.
Lean, the coding language these efforts revolve around, was invented more than a decade ago by a Microsoft researcher named Leonardo de Moura. He designed the language as a tool for human programmers, but now that AI technologies can generate their own computer code, they too can use Lean to write their own math proofs. Through extreme trial and error – a technique called “reinforcement learning” – an AI system can learn to write better Lean code and, ultimately, prove math problems that have flummoxed top mathematicians for decades.
Companies like &Truth aim to eliminate buggy software using similar techniques. The trouble is that training AI systems for code verification is significantly more difficult than training them for math.
Part of the problem is that software code is much messier than math. The rules of math are well established – and have been for centuries. To verify the integrity of a software application, someone must first lay down a set of formal specifications that define how the application is supposed to behave. Only then can an AI system write Lean code that verifies this behaviour.
Even then, applications may behave in unexpected and unwanted ways that allow malicious hackers into the system. An application’s designers cannot anticipate everything that will go wrong once they roll the application into the real world and real people start to use it.
“How do you know that your assumptions are correct?” said Will Wilson, CEO of Antithesis, a company that tests computer code for bugs and security holes. “At some point, code comes into contact with messy reality.”
At this point, companies like &Truth are a long way from ensuring that all software is bug-free. But at a moment when AI-enabled hacking is threatening online security like never before, any bit of progress helps.
“There is an urgency that was increasingly palpable beginning at the end of last year,” said Chris Hsu, &Truth’s co-founder and co-CEO. “This security problem is a defining problem of our time.” – ©2026 The New York Times Company
This article originally appeared in The New York Times.
