&Truth 获 7000 万美元种子轮，要用 Lean 构建代码通用验证机

&Truth 是一家致力于开发能够以数学方式证明软件安全性的技术的公益公司，于 2026 年 10 月 29 日结束隐身状态，披露了 7000 万美元种子轮融资，并公布了一项计划：构建其所谓的代码通用验证机。

在发布公告中，该公司表示其成立于 2026 年初，并获得了一笔 7000 万美元的种子资金，投资方被其描述为具有奠基意义的 AI 安全与风险投资领袖。该公司表示，其验证机旨在读取任何编程语言的代码，并以数学方式证明其安全、可靠且正确，且证明可供任何人独立核验。

基于 Lean 构建的证明自动化

公告称，形式化验证已存在数十年，但此前难以普及且成本高昂，因为专家必须手动构建证明，使这一实践仅限于少数关键系统。该公司表示，如今 AI 将形式化证明工作加速了 100 倍或更多，而其证明自动化技术又将这一过程进一步加速 100 倍，将证明生成从数年或数月缩短至数小时或数分钟。

该公司还介绍了其所谓的“规范工厂”技术，称该技术使企业和开发者能够大规模地将人类意图和业务需求转化为精确的形式化规范，从而产生可独立核验的保证，而非依赖测试或供应商的说法。

&Truth 正基于开源证明系统 Lean 和包含超过两百万行数学定义与定理的 Mathlib 库进行构建，并结合包括 CSLib 在内的开源技术。据该公司称，其目标是建立软件的通用形式化词汇表：编程语言和系统的数学模型、证明技术，以及能够实现跨语言自动化验证的精确规范。&Truth 表示，其与 Lean 聚焦研究组织合作，并打算将其基础库作为开源发布。

联合创始人兼联合首席执行官 Clark Barrett 表示，Lean 和 Mathlib 为 AI 提供了用于数学推理的精确语言，而软件一直缺乏同等的基础。联合创始人兼首席科学官 Ilya Sergey 表示，对软件的信任应建立在可独立核验的证明之上，而非任何公司的言辞。

创始人与双总部

Barrett 是斯坦福大学计算机科学 Corbel 讲席教授、斯坦福 AI 安全中心创始联合主任、斯坦福自动推理中心主任、CSLib 联合创建者，以及 cvc5 自动推理引擎的项目负责人。Sergey 在新加坡国立大学创立了 VERSE 实验室，并联合创建了开源验证器 Veil 和 Velvet。联合创始人、联合首席执行官兼执行主席 Chris Hsu 是 Lean FRO 战略顾问委员会成员、Infinitude Foundation 总裁，此前曾担任 Kilometre Capital 首席执行官以及 Citadel Investment Group 董事总经理。

公告还提到了 Gregory Malecha，他此前在 BlueRock Security 领导形式化方法，并且是 BRiCk 验证框架的关键架构师；Sebastian Ullrich，Lean 4 的联合架构师、Lean 聚焦研究组织的联合创始人；Linus Lee，Kilometre Capital 前管理合伙人；以及 Drew Harman，Fastino Labs 前首席商务官、Insight Partners 和 Shasta Ventures 的运营合伙人。&Truth 表示，其建立在斯坦福大学和新加坡国立大学数十年的形式化验证与自动推理研究基础之上。

&Truth 的美国总部位于帕洛阿尔托，国际总部位于新加坡，该公司表示其新加坡办公室将在研究、工程、产品和市场推广工作方面大幅扩张。新加坡数字产业发展司高级副总裁兼联合主管 Low Jin Yong 在公告中表示，该总部将深化新加坡的信任与安全能力，并巩固该国作为开发可信 AI 企业基地的地位。

该公司网站还刊登了一场圆桌讨论，参与者包括 Lean 的发明者、AWS 副总裁兼杰出科学家 Leonardo de Moura，以及 Lean FRO 战略顾问委员会成员、Google 杰出工程师 Simone Severini。

在 2026 年 10 月 29 日的一篇配套文章中，Hsu 详细阐述了该公司所称使验证变得紧迫的趋势，并援引 Google 首席执行官 Sundar Pichai 的言论称，Google 目前 75% 的新代码由 AI 生成并经工程师批准，以及 Veracode 2026 年的测试发现，AI 模型在近半数涉及安全性的编码任务中失败。该文章还援引了 2026 年 9 月的一次攻击活动：攻击者部署了数百个 AI 代理，通过广泛使用的打印管理软件中的漏洞入侵了 48 个国家的 395 个组织；以及 2026 年 9 月公布的创纪录的 14,959 个软件漏洞，该文章称这一数字是一年前公布数量的 3.5 倍。

该文章回顾了早先的形式化验证里程碑：seL4 微内核的原始证明针对约 8,700 行代码，耗费了约 20 人年的专家努力；2015 年，在 DARPA 的 HACMS 计划下，seL4 被集成到波音公司的无人小鸟直升机中，其飞行控制装置在专业红队获得数周访问权限的情况下仍无法被攻破；2026 年 9 月，Anthropic 开发的一个 AI 模型在 11 天内用 Lean 形式化了费马大定理的完整证明。文章还指出，2026 年早些时候，Lean FRO 的高级研究软件工程师 Kim Morrison 在极少人工指导下使用 Anthropic 的 Claude 构建了 zlib 压缩库的 Lean 版本，并证明它始终能精确还原其压缩的数据。

该文章引用了 Lean 创造者 Leonardo de Moura 的话：“测试提供信心。证明提供保证。”

在2026年10月29日发表的第二篇文章中，Sergey解释了程序验证的机制，从Alan Turing 1949年的论文《Checking a Large Routine》讲起，该论文提出程序员应随代码附带精确的声明，使检查器能够逐项验证。文章描述了在Lean中检查的规范、循环不变式和证明，并指出&Truth的目标是让开发者以使验证成为开发常规部分的成本，获得可独立检查的证据，例如Lean中的形式化证明。

&Truth将其长期愿景描述为从“氛围编程”转向“验证编程”，即AI生成的代码在部署前经过数学验证，AI代理在可证明受控的环境中运行，遗留软件得到安全现代化，关键基础设施受到可独立检查的数学保证的保护。