&Truth

Proving that a program does what it should, for every possible input, has long been reserved for chip designs, flight software and a few cryptographic libraries, because each proof took specialists months or years. &Truth was founded in early 2026 to change that arithmetic, using AI to write and check proofs at a speed it says turns months into minutes.

A formal vocabulary for software

The company builds on Lean, the open-source proof assistant, and on CSLib, an open library it helps develop. Its plan is a shared formal vocabulary for software: mathematical models of programming languages and systems, reusable proof techniques, and precise specifications that automated tools can verify across languages. The company claims AI already speeds up proof writing about a hundredfold and that its own proof automation adds another hundredfold on top.

A second strand, which &Truth calls a specification factory, turns human intent and business requirements into formal specifications, so that a proof has something exact to be checked against. The company says it will release its foundational libraries as open source and works with the Lean Focused Research Organization.

Founders from Stanford, NUS and finance

Clark Barrett, co-chief executive, is a computer science professor at Stanford who directs its Center for Automated Reasoning and leads the cvc5 solver project. Ilya Sergey, chief science officer, founded the VERSE Lab at the National University of Singapore. Chris Hsu, co-chief executive and executive chairman, sits on the Lean FRO's strategic advisory board and previously led Kilometre Capital. The team also includes Sebastian Ullrich, a co-architect of Lean 4, and Gregory Malecha, formerly head of formal methods at BlueRock Security.

Key facts

Founded: early 2026 Headquarters: Palo Alto, California (US) and Singapore (international) Legal form: public benefit corporation Funding: US$70 million seed, investors not named (announced 29 October 2026) Status: no product, pricing or customers published yet