&Truth 获 7000 万美元种子轮融资，旨在打造代码通用验证机

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

在发布公告中，该公司表示成立于 2026 年初，种子轮融资 7000 万美元，资金来自一批被其称为人工智能安全与风险投资领域先驱的领军人士。公司表示，其正在打造的验证机将能够读取任何编程语言编写的代码，并以数学方式证明代码安全、可靠且正确，而且任何人都可以独立核验这些证明。

基于 Lean 构建的证明自动化技术

公告称，形式化验证已有数十年历史，但过去难以普及且成本高昂，因为专家必须手动构造证明，导致这种实践仅限于少数关键系统。公司表示，如今人工智能可将形式化证明工作提速 100 倍以上，而其证明自动化技术还能在此基础上再提速 100 倍，将生成证明所需的时间从数年或数月缩短至数小时或数分钟。

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

&Truth 正在基于开源证明系统 Lean 和 Mathlib 构建，其配套资源包括一个包含逾 200 万行数学定义与定理的库，以及 CSLib 等开源技术。公司表示，其目标是为软件建立一套通用的形式化语言体系：涵盖编程语言和系统的数学模型、证明技术，以及能够支持跨语言自动化验证的精确规范。&Truth 表示，公司与 Lean Focused Research Organization 合作，并计划将其基础库开源。

联合创始人兼联席首席执行官 Clark Barrett 表示，Lean 和 Mathlib 为人工智能提供了一种能够进行数学推理的精确语言，而软件领域一直缺少同等的基础。联合创始人兼首席科学官 Ilya Sergey 表示，对软件的信任应建立在可独立核验的证明之上，而非任何一家公司的口头保证。

创始团队与双总部

Barrett 是 Stanford University 的 Corbel 计算机科学讲席教授、Stanford Center for AI Safety 创始联合主任、Stanford Center for Automated Reasoning 主任、CSLib 的共同创作者，也是自动推理引擎 cvc5 的项目负责人。Sergey 创立了 National University of Singapore 的 VERSE Lab，并共同开发了开源验证器 Veil 和 Velvet。联合创始人、联席首席执行官兼执行董事长 Chris Hsu 是 Lean FRO 战略顾问委员会成员，也是 Infinitude Foundation 的主席；此前，他曾担任 Kilometre Capital 首席执行官以及 Citadel Investment Group 董事总经理。

公告还介绍了 Gregory Malecha。他此前负责 BlueRock Security 的形式化方法工作，并是 BRiCk 验证框架的主要架构师；Sebastian Ullrich 是 Lean 4 的共同架构师，也是 Lean Focused Research Organization 的联合创始人；Linus Lee 曾任 Kilometre Capital 管理合伙人；Drew Harman 曾任 Fastino Labs 首席商务官，并担任 Insight Partners 和 Shasta Ventures 的运营合伙人。&Truth 表示，其工作建立在 Stanford University 和 National University of Singapore 数十年来在形式化验证与自动推理领域的研究成果之上。

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

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

配套文章阐述公司的发展缘由

在一篇日期为 2026 年 10 月 29 日的配套文章中，Hsu 详细阐述了公司认为让验证工作刻不容缓的趋势。他援引 Google 首席执行官 Sundar Pichai 的说法称，Google 目前 75% 的新代码由人工智能生成并经工程师批准；还提到 Veracode 于 2026 年开展的测试，结果发现，在安全性至关重要的编码任务中，人工智能模型有近一半未能完成。文章还提及 2026 年 9 月发生的一场攻击行动：攻击者部署数百个人工智能代理，利用广泛使用的打印管理软件中的漏洞，入侵了 48 个国家的 395 个组织；此外，2026 年 9 月发布的软件漏洞数量创下 14,959 个的纪录，文章称这一数字是前一年同期发布数量的 3.5 倍。

这篇文章回顾了形式化验证领域早期的里程碑：seL4 微内核最初的证明耗费了专家约 20 人年，涉及约 8,700 行代码；2015 年，在 DARPA 的 HACMS 计划下，seL4 被部署到波音公司的 Unmanned Little Bird 直升机上，一支获得数周访问权限的专业红队未能攻破其飞行控制系统；2026 年 9 月，Anthropic 开发的一个 AI 模型仅用 11 天，便在 Lean 中形式化完成了费马大定理的完整证明。文章还提到，2026 年早些时候，Lean FRO 的高级研究软件工程师 Kim Morrison 在 Anthropic 的 Claude 几乎没有人工指导的情况下，构建了一个 Lean 版本的 zlib 压缩库，并证明该库总能原样还原其压缩的数据。

文章引用了 Lean 的创作者 Leonardo de Moura 的话：“测试带来信心，证明则提供保证。”

在2026 年 10 月 29 日发表的另一篇文章中，Sergey 解释了程序验证的原理，首先回顾了 Alan Turing 1949 年发表的论文《检查大型程序》，该文提出，程序员应在代码旁附上精确的断言，供检查器逐一验证。文章介绍了规范、循环不变式以及经 Lean 检查的证明，并指出 &Truth 的目标是让开发者能够以足以使验证成为日常开发环节的成本，获得可独立检查的证据，例如 Lean 中的形式化证明。

&Truth 将其长期愿景描述为从“凭感觉编程”转向“可验证编程”：AI 生成的代码在部署前经过数学验证，AI 智能体在可证明受控的环境中运行，旧有软件得到安全现代化改造，关键基础设施则由可独立检查的数学保证加以保护。