A $70 million seed round is a statement in any year. At &Truth it is an argument: that formal verification — proving software correct mathematically instead of testing it — has been blocked by cost rather than by theory, and that generative AI can attack that cost directly.
The company emerged from stealth on 29 October as a public benefit corporation based in Palo Alto and Singapore, founded in early 2026. Its co-founders are Clark Barrett, a Stanford professor and co-director of the Stanford Center for AI Safety, as co-CEO; Ilya Sergey, founder of the VERSE Lab at the National University of Singapore, as chief science officer; and Chris Hsu as co-CEO and executive chairman. &Truth has not named its investors or disclosed terms.
The stack builds on the Lean proof system and open-source projects such as CSLib. &Truth pairs its own model with proof automation to read code in any programming language and produce claims about safety, security and correctness that anyone can independently check. Alongside it sits 'specification factory' technology that turns business requirements into precise formal specifications — in practice the harder half of the problem, because most codebases arrive with code but no usable spec.
The demonstration carrying the round came from Stanford researcher Chuyue Sun, who joined &Truth in August. Her team used AI to formally verify part of the encryption code in the Signal messaging app: under half a day of work, for less than $500. By hand, the company says, the same job would have taken three experienced engineers roughly five months.
'Bridges, buildings, they don't collapse, because people did math before constructing them,' Sergey said. 'Why don't we do the same for code? The technology to mathematically reason was all there, just difficult to scale.' Barrett drew the parallel to AI's recent run of proving open mathematical conjectures: the same formal methods apply to software.
&Truth is one of a wave. Rival Harmonic, backed including by Nvidia's venture arm, has raised $295 million and this week unveiled Aristotle, an agent that verifies C code and Verilog hardware designs; Tensordyne and Nvidia are reported to be evaluating it. Anthropic and verification startup Theorem jointly announced AI-assisted bug-finding across open-source software plus a verification add-on for Claude. Madan Musuvathi, formerly of Microsoft Research, formed Truidic to commercialise automated verification after a run of security incidents across the AI sector.
Scepticism is plentiful, and earned. Will Wilson, chief executive of bug-hunting startup Antithesis, called formal verification 'a trap on its own': his firm spent millions verifying defensive systems and still found further errors with testing tools. Ethereum creator Vitalik Buterin has warned that verification is not a panacea for vulnerabilities. Byron Cook, a distinguished scientist at AWS, says automated reasoning has eased customers' cloud-security worries — but midsized companies told Wired that waiting weeks for verification slows development, and that verification engineers are scarce.
That is the real bet: not that proofs are perfect, but that they become cheap enough to sit inside a normal development loop. At under $500 and half a day for a slice of Signal's encryption, the arithmetic is at least interesting.
