& Truth 融资 70M 种子用于构建通用验证机码

供资

& Truth 融资 70M 种子用于构建通用验证机码

在 Google 上的首选来源中添加 Unite.AI

2026年10月29日从隐蔽处出现，披露了7000万美元的种子资金

在其发布公告中，称公司成立于2026年初，由它描述为形成AI安全及风险投资领袖的集团提供7000万美元的种子资本。 称公司正在建造它的核查机，以读取任何编程语言的代码，并在数学上证明它是安全的，安全的，正确的，并有任何人可以独立检查的证据。

在 Lean 上建造的自动化证明

正式核查已经存在数十年，但以前是无法进入的，而且费用昂贵的公告称，因为专家必须手动提出证据，将这种做法限制在少数关键系统中。 称 AI公司现在以100x或以上的速度加速正式的证明工作，其证明自动化技术又以100x加速了这一过程，将证明生成从数年或数月减少到数小时或数分钟。

该公司还介绍了它所称的“规格工厂”技术，它使企业和开发商能够将人的意向和业务要求转化为规模化的精确的正式规格，产生可以独立检查的保证，而不是依靠测试或销售商声称。

& Truth在Lean，一个开源的证明系统之上，和Mathlib，一个拥有200多万行数学定义和定理的库，以及包括CSLib在内的开源技术。 公司认为，目标是软件的通用正式词汇：编程语言和系统的数学模型，证明技术，以及精确的规格，可以实现跨语言的自动化验证。 & Truth 称它与精益聚焦研究组织合作，并打算将其基础库作为开源发布。

共同Founder和共同CEO克拉克·巴雷特(Clark Barrett 称 Lean)和Mathlib为AI提供了在数学中推理的精确语言，而该软件缺乏同等的基础。 共同创始人兼首席科学官Ilya Sergey 称对软件的信任应该依靠可独立核查的证据，而不是任何公司的说法。

创始人和双重总部

巴雷特是斯坦福大学的Corbel计算机科学教授，斯坦福AI安全中心的创始共同主任，斯坦福自动化理性中心主任，CSLib的共同创造者，Cvc5自动推理引擎的项目领导。 谢尔盖在新加坡国立大学创建了VERSE实验室，并共同创建了开源验证器Veil和Velvet. 共同创始人，共同首席执行官，执行董事长克里斯·许(Chris Hsu)是精益FRO战略顾问委员会成员和Infinient基金会主席，之前曾担任Kilome Capital的首席执行官和Citadel投资集团的总裁。

该公告还命名为：之前在BlueRock Security领导正式方法的Gregory Malecha，是BriCk核查框架的主要设计师；Lean 4的共同建筑师和Lean Focused研究组织的共同创始人Sebastian Ullrich;Kilome Capital的前管理合伙人Linus Lee;Fastino Labs的前首席商业官Drew Harman和Insight Partners和Shasta Ventures的运营合伙人。 & Truth 称以斯坦福大学和新加坡国立大学数十年的正式核查和自动化推理研究为基础。

& Truth的美国总部位于Palo Alto，其国际总部位于新加坡，称公司的办公室将在研究、工程、产品和上市工作方面大幅扩展。 称在公告中表示总部将深化新加坡的信任和安全能力，加强国家作为公司开发可信赖AI的基地。

该公司的网站还设有一个圆桌讨论会，与Lean的发明者Leonardo de Moura和AWS的VP及杰出科学家，以及Simone Severini,Lean FRO战略顾问委员会成员和Google的杰出工程师。

公司的基本原理

在一份日期为2026年10月29日的配套论文中，Hsu详述了称公司将验证工作急迫化的趋势，引用了GoogleCEO孙达尔·皮凯的言论，即Google75%的新代码现在由AI生成并获得工程师批准，Veracode的2026测试发现AI模型在安全重要的近一半编码任务上失败。 文章还引用了2026年9月的一场运动，一名攻击者通过广泛使用的印刷管理软件的缺陷，部署数百个AI agents突破了48个国家的395个组织，2026年9月发表的创纪录的14,959个软件弱点，这个数字描述为一年前公布的3.5倍。

论文重述了早先正式验证的里程碑：seL4微内核的原始证明花了大约20个人年的专家努力，花了约8,700行代码；2015年，根据DARPA的HACMS计划，seL4被建在波音的无人小鸟直升机上，其飞行控制了一个专业的红色团队，获得数周的进入时间不能突破；2026年9月，Anthropic开发的AI模型将Fermat最后定理的完整证明在11天内正式化。 同样指出在2026年早些时候，Lean FRO的高级研究软件工程师金·莫里森(英语：Kim Morrison)利用Anthropic的Claude，在最低限度的人类引导下，建造了Lean版本的zlib压缩库，并证明它总是完全恢复其压缩的数据。

论文引用了精益创作者Leonardo de Moura的话说：“试验提供了信心。 证据提供了保证。”

在2026年10月29日出版的第二篇散文中，谢尔盖解释了程序验证的力学，从艾伦·图灵1949年的论文"检查大例程"开始，该论文建议程序员在代码上附上精确的声称，一个检查员可以单独验证。 文章描述了规格、循环变量和在Lean中检查的证明，并称 & Truth 的目的是让开发者获得独立可核查的证据，例如Lean的正式证据，费用使核查成为开发的例行部分。

& Truth将其长期愿景描述为从“vibe-coding”到“veri-coding”的转变，其中AI生成的代码在部署前经过数学验证，AI agents在可证明包含的环境内运行，遗留软件安全现代化，关键基础设施通过独立可验证的数学保证保护。

本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。

Funding

&Truth Raises $70M Seed to Build Universal Verification Machine for Code

Add Unite.AI to your preferred sources on Google

&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.

Auto-fetched and translated by AI Atlas. All rights belong to the original author.