&Truth, a public benefit corporation, is establishing a foundational standard for provably safe code. The company is building a universal verification machine to read code in any programming language and mathematically prove that it is safe, secure, and correct, with proofs that anyone can independently check.
As AI accelerates code generation and cyberattacks, proving whether software is safe has become increasingly urgent. Today, &Truth emerges from stealth to address this civilization-scale challenge. Founded in early 2026, &Truth was funded with $70 million of seed capital from a group of formative AI safety and venture capital leaders.
AI-generated code is being deployed faster than people can review it, while AI-powered attackers increasingly exploit vulnerabilities in the legacy software underpinning critical systems. Testing, monitoring, and code review remain essential but cannot guarantee that software behaves as intended. &Truth changes this, bringing mathematical assurance to software at scale.
Formal verification has existed for decades but was previously inaccessible and expensive. Experts had to manually formulate proofs, limiting verification to a handful of critical systems. AI now accelerates that process by 100x or more, and &Truth’s proof automation technology accelerates it by another 100x. By combining the two, &Truth is reducing proof generation from years or months to hours or minutes, making rigorous software verification cost-efficient and scalable.
&Truth is also pioneering “specification factory” technology. This enables enterprises and developers to translate human intent and business requirements into precise formal specifications at scale. The result is independently checkable guarantees beyond testing or vendor claims.
&Truth in action: see how we map and prove the vast ecosystem of the world’s critical software.
“AI transformed mathematics because Lean and Mathlib gave it a precise language for reasoning,” explains Clark Barrett, Co-Founder and Co-CEO of &Truth. “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.”
Lean, an open-source proof system, and Mathlib, a library of more than two million lines of mathematical definitions and theorems, have enabled breakthroughs in AI-assisted mathematics. Software presents a different challenge: many programming languages, constantly evolving codebases, and requirements often expressed imprecisely.
Building on Lean and open-source technologies including CSLib, &Truth is developing a universal formal vocabulary for software: mathematical models of programming languages and systems, proof techniques, and precise specifications that enable automated verification across languages and at scale.
“Trust in software should rest on independently checkable proof, not any company’s word, including ours,” says Ilya Sergey, Co-Founder and Chief Science Officer of &Truth. “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.”
&Truth works with the Lean Focused Research Organization and the broader open-source community and intends to release its foundational libraries as open source. Its public benefit mission is to help ensure AI develops safely for humanity.
“AI is now breaking code at superhuman speed. ‘Good enough’ is no longer enough. In the AI era, even 99% safe is certainly broken,” says Chris Hsu, Co-Founder, Co-CEO, and Executive Chairman of &Truth. “We must move from hoping code works to proving it does.”
&Truth builds on decades of pioneering research in formal verification and automated reasoning at Stanford University and the National University of Singapore, including foundational open-source technologies developed by its co-founders. Global from inception, &Truth has its U.S. headquarters in Palo Alto and its international headquarters in Singapore. Engineering and product teams in both locations lead coordinated workstreams to make mathematically verified software accessible and scalable worldwide.
&Truth’s Singapore office, already home to a world-class team in formal methods, AI, and systems engineering, will expand significantly across research, engineering, product, and go-to-market, while collaborating with Singapore’s institutions and industry on innovation, safe AI, and talent development.
“As AI adoption scales, trust and safety will become increasingly important to how companies can deploy AI with confidence. &Truth’s international headquarters in Singapore will deepen our capabilities in this area, while strengthening Singapore as a base for companies to develop trusted AI solutions,” said Low Jin Yong, Senior Vice President and Co-Head of Digital Industry Singapore.
The &Truth team brings together researchers and engineers in formal verification, theorem proving, programming languages, and Lean. Its leadership includes:
- Clark Barrett, Co-Founder and Co-CEO, the Corbel Professor of Computer Science at Stanford University, founding co-director of the Stanford Center for AI Safety, director of the Stanford Center for Automated Reasoning, co-creator of the open-source CSLib project, and project lead for the cvc5 automated reasoning engine.
- Ilya Sergey, Co-Founder and Chief Science Officer, founder of the VERSE Lab at the National University of Singapore, co-creator of the open-source verifiers Veil and Velvet.
- Chris Hsu, Co-Founder, Co-CEO, and Executive Chairman, Lean FRO Strategic Advisory Board member, the President of Infinitude Foundation, previously CEO of Kilometre Capital and Managing Director of Citadel Investment Group.
- Gregory Malecha, an expert in systems code verification and proof automation, previously leading formal methods at BlueRock Security; key architect of the BRiCk verification framework.
- Sebastian Ullrich, co-architect of Lean 4, a co-founder of the Lean Focused Research Organization, and a leading developer of the Lean theorem prover.
- Linus Lee, former Managing Partner at Kilometre Capital and software engineer at Athenahealth.
- Drew Harman, former Chief Commercial Officer at Fastino Labs, Operating Partner at Insight Partners and Shasta Ventures, and VP of Product and Strategy at Ariba.
&Truth envisions a safe AI future in which developers move from “vibe-coding” to fearless “veri-coding.” AI-generated code is mathematically verified before deployment, and AI agents operate within provably contained environments. Legacy software is modernized safely, and critical infrastructure is protected by independently checkable mathematical guarantees.
In that future, we place provable boundaries around increasingly powerful machines, ensuring they operate according to human intent.
It’s time to prove the code.
About &Truth
&Truth is a public benefit corporation building the universal verification machine for code. We’re establishing an open, independently checkable standard for provably safe software, proving that legacy and AI-generated code meets precise requirements. Founded in 2026 and based in Palo Alto and Singapore, &Truth is committed to ensuring AI develops safely for humanity.
Interested in verifying your critical code? Joining the &Truth mission? Learn more and contact us at andtruth.com.
View source version on businesswire.com: https://www.businesswire.com/news/home/20261029287395/en/
Media gallery
