&Truth emerges from stealth, pioneering the universal verification machine for code

This press release was issued by &Truth.


&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.

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.

&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.

&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.

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.