&Truth has emerged from stealth with $70 million in seed funding to build what it describes as a universal verification machine capable of mathematically proving that software is safe, secure, and correct across programming languages.
Founded in early 2026 as a public benefit corporation, &Truth is developing technology designed to address the growing risks created by rapidly expanding AI-generated software and increasingly sophisticated cyberattacks.
The company’s platform is based on formal verification, a method that uses mathematical proofs to determine whether software behaves according to specified requirements across all possible inputs.
Formal verification has existed for decades, but historically required significant manual work from highly specialized experts. &Truth said advances in AI can accelerate the proof-generation process by more than 100 times, while its own proof automation technology can add another 100-fold improvement.
The company believes this combination can reduce verification timelines from months or years to hours or minutes.
&Truth is also developing what it calls “specification factory” technology, which translates human intent and business requirements into precise mathematical specifications that software can be verified against.
Its technology builds on Lean, an open-source theorem-proving system, along with Mathlib and other open-source formal verification technologies including CSLib.
The company is working to create a universal formal vocabulary for software encompassing programming languages, system behaviors, proof techniques, and specifications.
&Truth plans to release foundational libraries as open source and is collaborating with the Lean Focused Research Organization and the broader open-source community.
The company operates from U.S. headquarters in Palo Alto and international headquarters in Singapore, with engineering and product teams in both locations.
Its leadership includes researchers and executives with backgrounds spanning Stanford University, the National University of Singapore, automated reasoning, formal methods, theorem proving, venture investing, and enterprise software.
Co-founder and co-CEO Clark Barrett is a Stanford University computer science professor and founding co-director of the Stanford Center for AI Safety. Ilya Sergey, co-founder and chief science officer, founded the VERSE Lab at the National University of Singapore. Chris Hsu serves as co-founder, co-CEO, and executive chairman.
&Truth ultimately envisions AI-generated software being mathematically verified before deployment, AI agents operating within provably contained environments, and critical software infrastructure protected by independently checkable guarantees rather than relying solely on testing and monitoring.
KEY QUOTES:
“AI transformed mathematics because Lean and Mathlib gave it a precise language for reasoning. Software has lacked an equivalent foundation. Once we can state precisely what code must do, AI can help prove that it does it, at a speed and scale previously out of reach.”
Clark Barrett, Co-Founder And Co-CEO Of &Truth
“Trust in software should rest on independently checkable proof, not any company’s word, including ours. Mathematical proof can establish that code meets precise requirements across all possible inputs, under clearly stated assumptions. Our mission is to bring that level of trust to the world’s software.”
Ilya Sergey, Co-Founder And Chief Science Officer Of &Truth
“AI is now breaking code at superhuman speed. ‘Good enough’ is no longer enough. In the AI era, even 99% safe is certainly broken. We must move from hoping code works to proving it does.”
Chris Hsu, Co-Founder, Co-CEO, And Executive Chairman Of &Truth
