AI 推动形式化验证创业潮，&Truth 融资 7000 万美元

斯坦福大学研究员Chuyue Sun与她的计算机科学家同行开发了一款AI工具，在不到半天时间内、花费不到500美元就完成了一个工程项目，而三位高技能专家手工完成同样的工作则耗时五个月。Sun在最近的一篇论文中报告的这一时间和成本的大幅缩减，正是唤醒一个鲜为人知的编程与数学领域——形式化验证——的早期成果之一。

数十年来，开发者一直设想用数学来证明他们的软件没有缺陷。这一过程漫长而艰辛，需要工程师就软件的目标写出精确的陈述，并将代码转换为可被验证的公式。尽管企业已经运行复杂的测试来尽可能多地找出软件中的缺陷，但它们很少花钱去做形式化验证，而形式化验证能够捕捉到甚至更多异常行为。

如今，一批初创公司正押注生成式AI将使形式化软件验证既切实可行又不可或缺。其中之一便是&Truth，Sun于8月加入该公司，该公司于周四公开上线。Sun的研究通过使用AI验证消息应用Signal中用于加密对话的部分代码，展示了这项技术的潜力。

“桥梁、建筑之所以不会坍塌，是因为人们在建造之前做了数学计算，”&Truth首席科学官Ilya Sergey说。“为什么我们不对代码做同样的事呢？进行数学推理的技术一直都有，只是难以规模化。”

&Truth已从投资者处筹集7000万美元，目标是最终能够验证任何编程语言。竞争对手Harmonic由Robinhood CEO Vlad Tenev联合创立，已获得2.95亿美元融资，本周宣布其专注于数学的AI智能体Aristotle支持验证用C语言编写的软件和用Verilog编写的硬件设计。该公司正在与潜在用户评估这项技术，包括芯片制造商Tensordyne和Nvidia，后者的风险投资部门是该初创公司的投资者之一。

就在上周，Anthropic与验证初创公司Theorem联合宣布，他们利用AI协助发现了开源软件中的缺陷，而这些缺陷是数万亿次测试都未能检测到的。他们还为Claude推出了一款附加组件，以帮助其他开发者进行验证。初始项目的成本未予披露。

最大的愿景是这样一个未来：软件运行更可靠，安全问题更少。但AI能否将形式化验证从NASA和Apple等组织中最关键的系统推广到广泛使用，仍是一个悬而未决的问题。

这项技术仍处于原型阶段。尽管需求很高，但客户愿意支付多少以及他们偏好如何采用这项技术尚不清楚。形式化验证依赖于对计算机和人如何与软件交互做出假设，一些专家对其捕捉由用户错误和硬件故障引发的缺陷的能力持怀疑态度。

经营缺陷搜寻AI软件初创公司Antithesis的Will Wilson称形式化验证对他这样的数学迷来说是“一个陷阱”。Antithesis花费数百万美元对其部分网络安全防御进行了形式化验证，Wilson称这一过程“令人痛苦不堪”。然而该初创公司仍用自家工具发现了更多错误，Antithesis还在其多家客户已进行形式化验证的软件中发现了缺陷。“它能给你一些保证，但只有稳健的穷尽式测试才能证明你的保证是真实的，”Wilson说。

或者正如因创造以太坊加密货币而闻名的工程师Vitalik Buterin在今年早些时候的一篇博客文章中所说，“形式化验证并非万灵药。”但他和其他支持这一方法的人仍然相信，它将成为抵御AI系统发动网络攻击和造成破坏的重要防线。

核心安全

根据公司披露，波音飞机、亚马逊服务器以及超过25亿台活跃的Apple设备中至少包含一些经过形式化验证的软件。相关代码通常与安全有关，其中的漏洞若被利用可能造成严重危害。

亚马逊云服务（AWS）的杰出科学家兼副总裁Byron Cook表示，形式化验证缓解了客户对云安全的担忧，并通过尽早消除重大缺陷帮助内部团队加快了进度。

但多家中型科技公司告诉《连线》，它们通常只对产品的一个关键功能进行了验证，甚至完全没有验证。它们提到缺乏验证工程师、成本超过潜在风险，以及或许最重要的一点——担心等待数周才能完成代码的形式化验证可能会拖慢创新。

今年早些时候，Apple 的安全团队表示，形式化验证在其用于加密的“corecrypto”库中发现的一些问题，用其他任何方式都不可能发现。但该公司补充说，在向 corecrypto 添加新代码时必须“保守”，以确保能够跟上审查的节奏。

两家尚未对任何代码进行形式化验证的大型公司的两位网络安全高管表示，他们不确定自动化是否会让这件事值得做。但这两位未获授权公开发言的高管表示，他们可以想象向大型 AI 实验室付费购买“经过验证的”AI 生成代码。

开源软件项目是许多应用的基石，其开发者正越来越多地尝试 AI 辅助验证。非营利组织 Beneficial AI Foundation 今年利用 Anthropic 的一笔资助，验证了与 Sun 在斯坦福所验证的相同的加密代码。名为 curve25519-dalek 的库的维护者 Michael Rosenberg 希望，持续验证工作能获得可持续的资金支持。“不过，我完全不知道这要如何实现，而且我们当然不应该依赖 AI 公司的善意，”他说。

一些急于扩展验证业务的初创公司也不确定，是应该直接将工具部署给客户，还是通过 Anthropic 这样的中间商来部署。它们的大致计划是利用 AI 来自动完成定义程序应如何行为所涉及的大量工作。例如，数据表的规范可能要求它在排序前后包含相同的条目，只是顺序不同。进一步的自动化工作（可能不涉及 AI）会将代码转换为 Lean、Rocq 和 Isabelle 等数学工具可用的格式，以检查代码是否按预期运行。

形式化验证领域另一位新近入局者是 Madan Musuvathi，他在微软研究院工作二十多年后离职，创办了初创公司 Truidic。在发生 OpenAI 入侵 Hugging Face 等事件后，他感到迫切需要将自己的研究商业化。“AI 落入攻击者手中可能极其强大，”Musuvathi 说，但验证可以“让 AI 对每个人、每个地方都安全可靠。”

Proofcraft 是少数长期提供传统验证的公司之一，它表示，人们对这一流程日益高涨的热情正转化为潜在客户的大量咨询。该公司 CEO June Andronick 和首席科学家 Gerwin Klein 表示，兴趣很容易超出他们及其竞争对手所能提供的范围。

但两人都担心，AI 生成的规范可能会让人对结果产生“毫无根据的信任”。验证者也渴望保留这项工作带给他们的乐趣。Klein 称它“相当令人上瘾，就像解谜游戏。”如果一切顺利，他将比以往任何时候都更多地解题。

直达你的收件箱：通过 Kernel Panic 深入了解数字安全世界

我们与一个 Muse AI 智能体互发了色情短信——而 Meta 说这完全没问题

重磅报道：认识 DEA 首屈一指的加密货币侦探

OpenAI 正在惹恼数学家