THE ESSENTIALS IN 30 SECONDS

  • &Truth announced on October 29 that it raised $70 million in seed capital; the backers are described only as AI safety and venture capital leaders.
  • The company is building what it calls a universal verification machine, meant to prove code in any language safe, secure and correct, on top of the Lean proof system.
  • Co-founders include Stanford professor Clark Barrett and Ilya Sergey of the National University of Singapore; speed-up claims are not independently verified.

A new startup wants to replace trust in AI-generated code with mathematical proof. &Truth, a public benefit corporation founded in early 2026, came out of stealth on October 29 with $70 million in seed funding, according to a press release distributed by Business Wire from Palo Alto and Singapore. The company has not named its investors, describing them only as leaders in AI safety and venture capital.

What the company is building

&Truth says it is developing a "universal verification machine" for software: a system that reads code written in any programming language, attempts to prove that it is safe, secure and correct, and outputs proofs that third parties can check independently. It relies on Lean, an open-source proof assistant, and its large Mathlib library of formalised mathematics, as well as CSLib, a computer science library. The company also describes a "specification factory" meant to turn business requirements into formal specifications that proofs can be checked against. It says it will release its foundational libraries as open source and works with the Lean Focused Research Organization.

The founding team comes largely from formal methods research. Co-CEO Clark Barrett is a Stanford computer science professor who leads the cvc5 reasoning engine project; chief science officer Ilya Sergey founded the VERSE Lab at the National University of Singapore; and co-CEO and executive chairman Chris Hsu is a former CEO of Kilometre Capital. The US headquarters is in Palo Alto, while Singapore hosts the international headquarters, where the company plans to expand.

Claims and caveats

The pitch rests on the gap between how fast AI writes code and how slowly humans can review it. Hsu frames the stakes bluntly: "In the AI era, even 99% safe is certainly broken." The company claims AI already speeds up proof generation by 100 times or more and that its own automation adds another 100-fold gain, cutting work that took months or years to hours or minutes. It has published no benchmarks to support those figures.

TokenPost also notes a structural limit of the approach: a proof only guarantees what the specification states, under the model of the system used. It cannot show that the requirements capture everything users need or that the model matches every real-world condition. Formal verification has historically been costly; Unite.AI recalls that the seL4 kernel proof took about 20 person-years for roughly 8,700 lines of code. Whether &Truth can make such guarantees routine for everyday software is the open question.