&Truth emerges from stealth with a $70 million seed to mathematically verify code

&Truth came out of stealth on October 29 with $70 million in seed funding to build what it calls a "universal verification machine" for software. The company, a public benefit corporation founded in early 2026, has its US headquarters in Palo Alto and its international headquarters in Singapore. Its announcement describes the backers only as a group of AI safety and venture capital leaders; it did not name them or disclose a valuation.

The co-founders are Clark Barrett, co-CEO, a Stanford computer science professor, founding co-director of the Stanford Center for AI Safety and project lead for the cvc5 reasoning engine; Ilya Sergey, chief science officer, who founded the VERSE Lab at the National University of Singapore; and Chris Hsu, co-CEO and executive chairman, a former CEO of Kilometre Capital and former managing director at Citadel Investment Group. The team also includes Sebastian Ullrich, a co-architect of Lean 4.

What it says it is building

&Truth says its system will read code in any programming language and produce mathematical proofs that the code is safe, secure and correct, proofs that anyone can check independently. It builds on Lean, an open-source proof system, along with the Mathlib library and CSLib, and says it will release its foundational libraries as open source while working with the Lean Focused Research Organization. A second piece, which it calls a "specification factory," is meant to turn business requirements into formal specifications at scale.

The company claims AI already speeds up proof generation by 100x or more and that its own automation adds another 100x, cutting the work from months or years to minutes or hours. Those figures are &Truth's own and come without a public benchmark. The announcement names no customers and no generally available product. "In the AI era, even 99% safe is certainly broken," Hsu said. Sergey said: "Trust in software should rest on independently checkable proof, not any company's word, including ours."

Why it matters

As coding agents write more of a company's software, the expensive step moves from writing code to confirming it does what it should. A $70 million seed for formal verification is a sign that investors expect that review cost to become a market of its own. For teams buying AI coding tools today, nothing here changes the controls you need now: tests, code review and limits on what agents can deploy. It is worth tracking whether &Truth ships something that works on ordinary business code, and at what price, because a cheap proof of correctness would change how much of an agent's output you can accept without a person checking it.