&Truth emerges from stealth with $70M seed to mathematically prove code is safe
What's the deal? &Truth, a public benefit corporation founded in early 2026, has emerged from stealth with $70 million in seed funding from a group of AI safety and venture capital leaders.
What does it do? The company is building a universal verification machine that reads code in any programming language and mathematically proves it is safe, secure and correct, with proofs anyone can independently check. Building on the Lean proof system and open-source projects such as CSLib, &Truth combines AI with its own proof automation to bring formal verification, historically slow and expensive, to software at scale. It is also developing 'specification factory' technology that turns business requirements into precise formal specifications.
Who is behind it? Co-founders Clark Barrett (Co-CEO; Stanford professor and co-director of the Stanford Center for AI Safety), Ilya Sergey (Chief Science Officer; founder of the VERSE Lab at the National University of Singapore) and Chris Hsu (Co-CEO and Executive Chairman). &Truth has headquarters in Palo Alto and Singapore.
How was it demonstrated? Stanford researcher Chuyue Sun, who joined &Truth in August, showed the approach working on live code: her team used AI to formally verify part of the encryption code in the messaging app Signal, a project that took under half a day and less than $500, versus roughly five months of work for three experienced engineers doing it by hand. "Bridges, buildings, they don't collapse, because people did math before constructing them," said Ilya Sergey. "Why don't we do the same for code? The technology to mathematically reason was all there, just difficult to scale." Clark Barrett drew the same parallel to AI's recent run of proving unsolved math problems: "You've seen what has happened in mathematics — proving these massive open conjectures. We can apply the same formal methods to verifying software."
Where it sits: &Truth is one of a wave of startups betting that generative AI can make formal software verification practical at last. Rival Harmonic, which has raised $295 million including from Nvidia's venture arm, this week unveiled its Aristotle agent for verifying C code and Verilog hardware designs, while Anthropic and verification startup Theorem jointly announced AI-assisted bug-finding across open-source software. &Truth itself has not named its seed investors or disclosed the round's terms.
Source: &Truth press release, Business Wire, 29 October 2026
Source: Wired, 29 October 2026
Source: The New York Times, 29 October 2026
Image credit: Generated with Gemini
