&Truth 獲 $70M 種子輪融資，計劃打造通用程式碼驗證機

&Truth, a public benefit corporation developing technology to mathematically prove that software is safe, emerged from stealth on October 29, 2026, disclosing $70 million in seed funding and a plan to build what it calls a universal verification machine for code.

In its launch announcement, the company said it was founded in early 2026 and was funded with $70 million of seed capital from a group it described as formative AI safety and venture capital leaders. The company said its verification machine is being built to read code in any programming language and mathematically prove that it is safe, secure, and correct, with proofs that anyone can independently check.

Proof Automation Built on Lean

Formal verification has existed for decades but was previously inaccessible and expensive, the announcement said, because experts had to formulate proofs manually, limiting the practice to a handful of critical systems. The company said AI now accelerates formal proof work by 100x or more, and that its proof automation technology accelerates the process by another 100x, reducing proof generation from years or months to hours or minutes.

The company also described what it calls “specification factory” technology, which it said enables enterprises and developers to translate human intent and business requirements into precise formal specifications at scale, producing guarantees that can be checked independently rather than resting on testing or vendor claims.

&Truth is building on Lean, an open-source proof system, and Mathlib, a library of more than two million lines of mathematical definitions and theorems, together with open-source technologies including CSLib. The goal, according to the company, is a universal formal vocabulary for software: mathematical models of programming languages and systems, proof techniques, and precise specifications that enable automated verification across languages. &Truth said it works with the Lean Focused Research Organization and intends to release its foundational libraries as open source.

Co-Founder and Co-CEO Clark Barrett said Lean and Mathlib gave AI a precise language for reasoning in mathematics, and that software has lacked an equivalent foundation. Co-Founder and Chief Science Officer Ilya Sergey said trust in software should rest on independently checkable proof rather than any company’s word.

Founders and Dual Headquarters

Barrett is the Corbel Professor of Computer Science at Stanford University, founding co-director of the Stanford Center for AI Safety, director of the Stanford Center for Automated Reasoning, co-creator of CSLib, and project lead for the cvc5 automated reasoning engine. Sergey founded the VERSE Lab at the National University of Singapore and co-created the open-source verifiers Veil and Velvet. Co-Founder, Co-CEO, and Executive Chairman Chris Hsu is a member of the Lean FRO Strategic Advisory Board and president of Infinitude Foundation, and previously served as CEO of Kilometre Capital and as a managing director of Citadel Investment Group.

The announcement also named Gregory Malecha, who previously led formal methods at BlueRock Security and was a key architect of the BRiCk verification framework; Sebastian Ullrich, co-architect of Lean 4 and a co-founder of the Lean Focused Research Organization; Linus Lee, a former managing partner at Kilometre Capital; and Drew Harman, a former chief commercial officer at Fastino Labs and an operating partner at Insight Partners and Shasta Ventures. &Truth said it builds on decades of research in formal verification and automated reasoning at Stanford University and the National University of Singapore.

&Truth’s U.S. headquarters is in Palo Alto and its international headquarters is in Singapore, where the company said its office will expand significantly across research, engineering, product, and go-to-market work. Low Jin Yong, Senior Vice President and Co-Head of Digital Industry Singapore, said in the announcement that the headquarters will deepen trust-and-safety capabilities in Singapore and strengthen the country as a base for companies developing trusted AI.

The company’s website also features a roundtable discussion with Leonardo de Moura, the inventor of Lean and a VP and Distinguished Scientist at AWS, and Simone Severini, a Lean FRO Strategic Advisory Board member and a Distinguished Engineer at Google.

Companion Essays Detail the Company’s Rationale

In a companion essay dated October 29, 2026, Hsu detailed the trends the company says make verification urgent, citing remarks by Google CEO Sundar Pichai that 75% of new code at Google is now AI-generated and approved by engineers, and Veracode’s 2026 testing, which found that AI models failed on nearly half of the coding tasks where security mattered. The essay also cites a September 2026 campaign in which an attacker deployed hundreds of AI agents to breach 395 organizations across 48 countries through flaws in widely used print-management software, and a record 14,959 software vulnerabilities published in September 2026, a figure it describes as 3.5 times the number published a year earlier.

The essay recounts earlier formal-verification milestones: the seL4 microkernel’s original proof took roughly 20 person-years of expert effort for about 8,700 lines of code; in 2015, under DARPA’s HACMS program, seL4 was built into Boeing’s Unmanned Little Bird helicopter, whose flight controls a professional red team given weeks of access could not breach; and in September 2026 an AI model developed by Anthropic formalized the complete proof of Fermat’s Last Theorem in Lean in 11 days. It also notes that earlier in 2026, Kim Morrison, a senior research software engineer at the Lean FRO, used Anthropic’s Claude with minimal human guidance to build a Lean version of the zlib compression library and prove that it always restores exactly the data it compressed.

The essay quotes Lean creator Leonardo de Moura: “Testing provides confidence. Proof provides a guarantee.”

In a second essay published October 29, 2026, Sergey explains the mechanics of program verification, beginning with Alan Turing’s 1949 paper “Checking a Large Routine,” which proposed that programmers accompany their code with precise claims that a checker could verify individually. The essay describes specifications, loop invariants, and proofs checked in Lean, and states that &Truth’s aim is for developers to obtain independently checkable evidence, such as a formal proof in Lean, at a cost that makes verification a routine part of development.

&Truth describes its long-term vision as a shift from “vibe-coding” to “veri-coding,” in which 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.