The startup, founded by researchers from Stanford and the National University of Singapore, wants to make mathematical proof a standard part of software development.
AI can now write software in minutes. Proving that software is safe is another matter entirely.
A startup called &Truth has emerged from stealth with $70 million in seed funding to tackle that problem, bringing together researchers who have spent decades developing mathematical techniques for verifying computer programs.
Founded earlier this year by Stanford professor Clark Barrett, National University of Singapore researcher Ilya Sergey and investor Chris Hsu, the company is building what it calls a universal verification machine: software designed to mathematically prove that code behaves according to specified requirements.
&Truth has not disclosed its investors, valuation or paying customers. Its US headquarters are in Palo Alto, with an international headquarters in Singapore.
The idea behind the company comes from a field of computer science known as formal verification.
Traditional software testing checks whether a program works under selected conditions. Engineers write tests, run the software and investigate failures. But even a comprehensive testing system cannot examine every possible input or sequence of events.
Formal verification takes a different approach. It expresses requirements as mathematical statements, then establishes whether the program satisfies them under explicitly defined assumptions.
Consider a banking application that transfers money between accounts. Testing can check thousands of transactions. A mathematical proof could establish that, for the operations covered by the specification, money cannot be created or lost regardless of the permitted transaction sequence.
The difficulty is that constructing those proofs has historically required highly specialized engineers and substantial time.
That is beginning to change.
In research described in a recent paper, Stanford computer scientist Chuyue Sun and her colleagues developed an AI system called CryptoProver that generated machine-checked proofs for production cryptographic software.
The system completed one verification task in 11.4 hours, consuming approximately $467 in recorded API costs. An earlier independent, human-led verification effort had taken eight months of public development involving five main contributors.
The research covered cryptographic libraries associated with technologies used by applications including Signal. Sun joined &Truth in August, and Barrett was among the paper's authors.
The experiment demonstrates how AI could reduce the labor involved in formal verification. It does not establish that &Truth's commercial platform can already verify arbitrary software.
That remains the company's larger ambition.
Its architecture builds on Lean, an open-source proof assistant that checks mathematical proofs, and Mathlib, an extensive library of mathematical definitions and theorems.
Lean has become increasingly important in AI-assisted mathematics because models can generate candidate proofs that a separate system then checks mechanically.
&Truth wants to extend that approach to software engineering.
The company is developing reusable mathematical descriptions of programming languages, computer systems and software behavior. It is also building tools that translate requirements written by humans into precise specifications.
That second problem may prove particularly difficult. A proof can establish that software satisfies a specification, but it cannot guarantee that the specification describes what the user actually wanted.
&Truth says improvements in AI-assisted theorem proving have already accelerated parts of the verification process by more than 100 times. It claims its own automation could deliver another substantial improvement.
Those performance claims have not been independently demonstrated across a broad range of production systems.
The startup is entering a market attracting serious investment. Harmonic, co-founded by Robinhood CEO Vlad Tenev, has received $295 million in funding and is developing Aristotle, an AI agent that can produce mathematical proofs. Anthropic has also worked with Theorem on AI-assisted verification of open-source software.
There are reasons to be cautious about how widely the technology can be deployed.
Formal verification has been used for years in security-sensitive applications, but it remains expensive, difficult to maintain and dependent on the assumptions built into each specification. It cannot eliminate every failure caused by hardware, system integration or incorrect requirements.
And even mathematically verified programs still need conventional testing.
&Truth is structured as a public benefit corporation and says it intends to release its foundational libraries as open source, allowing external researchers to inspect and independently check its work.
The company has not announced a commercial launch date or explained how it intends to charge customers.
For now, the $70 million investment is a bet that the rapid growth of AI-generated software will create demand for something that conventional coding assistants cannot provide: independent mathematical evidence that the code does what its developers intended.
Sources: Wired · Announcement · CryptoProver paper · Team