&Truth raises $70m seed to prove code safe with AI-built proofs

&Truth raises $70m seed to prove code safe with AI-built proofs

29 October 2026: &Truth, a public benefit corporation founded in early 2026, has come out of stealth with US$70 million of seed funding to make formal verification, mathematical proof that code does what it should, cheap enough to apply to ordinary software. The company says the money came from "a group of formative AI safety and venture capital leaders" but names none of them.

Not yet independently verified. The release names no investors beyond "AI safety and venture capital leaders", and the speed-up figures are the company's own claims; no product or customer is public yet. We will update this when it can be confirmed, and remove this note.

What the company is building

Formal verification has been used for decades on a small number of critical systems, because experts had to write proofs by hand. &Truth argues that AI now speeds that work up by 100 times or more, and that its own proof automation adds another factor of 100, cutting proof generation "from years or months to hours or minutes". Both figures are the company's.

It is building on Lean, the open-source proof assistant behind recent advances in AI-assisted mathematics, and on CSLib. The aim is a "universal formal vocabulary" for software: mathematical models of programming languages and systems, proof techniques and precise specifications. A second piece, which it calls a specification factory, turns business requirements into formal specifications that a proof can then be checked against. &Truth says it works with the Lean Focused Research Organization and intends to release its foundational libraries as open source.

"Trust in software should rest on independently checkable proof, not any company's word, including ours," said Ilya Sergey, co-founder and chief science officer.

Who is behind it

The three co-founders come from research and finance. Clark Barrett, co-chief executive, is a professor of computer science at Stanford, directs its Center for Automated Reasoning and leads the cvc5 solver project. Sergey founded the VERSE Lab at the National University of Singapore. Chris Hsu, co-chief executive and executive chairman, previously ran Kilometre Capital and was a managing director at Citadel. The wider team includes Sebastian Ullrich, a co-architect of Lean 4, and Gregory Malecha, who led formal methods at BlueRock Security.

&Truth has its US headquarters in Palo Alto and an international headquarters in Singapore, where it plans to grow research, engineering, product and sales teams. Digital Industry Singapore, the government office for the digital sector, welcomed the move in the release.

Where it would sit for buyers

Nothing is for sale yet: the release describes technology and a mission, not a product, a price or a customer. The case it makes is aimed at teams shipping code written by AI faster than people can review it, and at operators of older critical software. "In the AI era, even 99% safe is certainly broken," said Hsu.

Company profile on TrustList: &Truth

Related on TrustList:

• Klarent raises $8m to bring AI-written software tests to the US

Sources

• &Truth: &Truth emerges from stealth, 29 October 2026