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

&Truth 是一家开发以数学方式证明软件安全性技术的公益公司（public benefit corporation），于 2026 年 10 月 29 日走出隐身模式，披露 7000 万美元种子轮融资，并计划打造其所谓的代码通用验证机（universal verification machine for code）。公司在发布公告中称，其创立于 2026 年初，7000 万美元种子资金来自一个被其描述为 AI 安全与风险投资领域奠基性人物的团体。该公司表示，其验证……

&Truth 是一家开发以数学方式证明软件安全性技术的公益公司（public benefit corporation），于 2026 年 10 月 29 日走出隐身模式，披露了 7000 万美元种子轮融资，并计划打造其所谓的代码通用验证机（universal verification machine for code）。

在其发布公告中，该公司表示自己创立于 2026 年初，7000 万美元种子资金来自一个被其描述为 AI 安全与风险投资领域奠基性人物的团体。公司称，其验证机旨在读取任何编程语言的代码，并以数学方式证明其安全、可靠且正确，其证明任何人都可独立核查。

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

该公司还介绍了其所谓的「规格工厂」（specification factory）技术，称其能让企业和开发者将人类意图与业务需求大规模转化为精确的形式化规格，产出可独立核查的保证，而非依赖测试或厂商的口头承诺。

&Truth 构建在开源证明系统 Lean 与 Mathlib 之上——后者是一个超过 200 万行的数学定义与定理库——并结合 CSLib 等开源技术。据公司介绍，其目标是为软件建立一套通用形式化词汇：编程语言与系统的数学模型、证明技术，以及能支持跨语言自动化验证的精确规格。&Truth 表示其与 Lean Focused Research Organization 合作，并打算将其基础库以开源形式发布。

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

Barrett 是斯坦福大学计算机科学 Corbel 讲席教授、斯坦福 AI 安全中心（Stanford Center for AI Safety）创始联席主任、斯坦福自动推理中心（Stanford Center for Automated Reasoning）主任、CSLib 共同创造者，以及 cvc5 自动推理引擎项目负责人。Sergey 在新加坡国立大学创立了 VERSE Lab，并共同创造了开源验证器 Veil 与 Velvet。联合创始人、联席 CEO 兼执行董事长 Chris Hsu 是 Lean FRO 战略顾问委员会成员、Infinitude Foundation 主席，曾任 Kilometre Capital CEO 及 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 表示，其建立在斯坦福大学与新加坡国立大学数十年形式化验证与自动推理研究的基础之上。

&Truth 的美国总部位于 Palo Alto，国际总部位于新加坡。公司表示，其新加坡办公室将在研究、工程、产品与市场拓展工作上大幅扩张。新加坡数字产业部门（Digital Industry Singapore）高级副总裁兼联席主管 Low Jin Yong 在公告中表示，该总部将深化新加坡的可信与安全（trust-and-safety）能力，并强化该国作为可信 AI 企业基地的地位。

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

在 2026 年 10 月 29 日发布的一篇配套文章中，Hsu 详述了该公司认为使验证变得紧迫的趋势，援引 Google CEO Sundar Pichai 的说法——Google 现有 75% 的新代码由 AI 生成、由工程师审核批准——以及 Veracode 2026 年的测试：其发现 AI 模型在约一半涉及安全的编程任务上失败。文章还引用了 2026 年 9 月的一次攻击行动：攻击者部署数百个 AI 代理，利用广泛使用的打印管理软件中的缺陷，入侵了 48 个国家的 395 个组织；以及 2026 年 9 月创纪录披露的 14959 个软件漏洞——该公司称这一数字是（原文正文至此截断）的 3.5 倍。