A Universal Verification Machine for Code

&Truth, a public benefit corporation founded in early 2026, has emerged from stealth with US $70 million in seed funding to build what it calls a universal verification machine — software designed to read code in any programming language and mathematically prove that it is safe, secure and correct, with proofs that anyone can independently check.

The company is positioning its platform as a foundational standard for provably safe code at a moment when AI-generated software is being deployed faster than human reviewers can audit it, and AI-powered attackers are increasingly exploiting vulnerabilities in the legacy systems underpinning critical infrastructure.

The seed round was backed by a group of formative AI safety and venture capital leaders, and the company is global from inception: its U.S. headquarters sits in Palo Alto, while Singapore serves as its international headquarters. Engineering and product teams in both locations will lead coordinated workstreams to make mathematically verified software accessible and scalable worldwide.

The Need for Mathematical Proof

&Truth frames its mission around a single premise: testing, monitoring and code review remain essential but cannot guarantee that software behaves as intended.

The company argues that mathematical proof is the only way to establish that code meets precise requirements across all possible inputs, under clearly stated assumptions. That conviction runs through the leadership bench, which draws on decades of formal verification research at Stanford University and the National University of Singapore.

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, &Truth

The company also leans on the analogy that transformed AI-assisted mathematics. Lean, an open-source interactive proof system, paired with Mathlib — a library of more than two million lines of mathematical definitions and theorems — gave machines a precise language for reasoning about math. &Truth is attempting to build the equivalent foundation for software.

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, &Truth

Architectural Approach and Benchmarks

Formal verification — the discipline of producing mathematical proofs that software satisfies a specification — has existed for decades but was historically inaccessible. Experts had to formulate proofs by hand, limiting the practice to a handful of safety-critical systems such as aerospace controllers and cryptographic kernels.

&Truth's bet is that AI collapses that bottleneck. The company says AI accelerates proof generation by 100x or more, and that its own proof automation technology adds another 100x on top of that. Combined, the company claims proof timelines shrink from years or months to hours or minutes, making rigorous verification cost-efficient for mainstream enterprise workloads.

The platform is built on Lean and open-source technologies including CSLib, and is being extended into 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.

Alongside the verification engine, &Truth is pioneering what it calls "specification factory" technology, which translates human intent and business requirements into precise formal specifications at scale — the step that has historically blocked verification projects before a single proof is attempted.

The company intends to release its foundational libraries as open source and is working with the Lean Focused Research Organization and the broader open-source community. Its public benefit mission is to help ensure AI develops safely for humanity, and its leadership is explicit about the stakes.

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, &Truth

Regional Rollout and Market Impact

Singapore is central to &Truth's go-to-market strategy. The company's Singapore office is already home to a team in formal methods, AI and systems engineering, and will expand significantly across research, engineering, product and go-to-market.

The expansion is being coordinated with Singapore's institutions and industry on innovation, safe AI and talent development, positioning the city-state as a hub for trusted AI infrastructure in the region.

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.

—Low Jin Yong, Senior Vice President and Co-Head, Digital Industry Singapore

&Truth's longer-term vision extends beyond static code review. The company describes a future in which developers move from "vibe-coding" to "veri-coding," where AI-generated code is mathematically verified before deployment, 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, the company argues, provable boundaries are placed around increasingly powerful machines to ensure they operate according to human intent.