AI 智能体参与 Signal 协议形式化验证

AI 能不能帮人证明加密协议是安全的？这篇报道给出的案例是：Google DeepMind 的 AlphaProof Code 用 Gemini 驱动的多智能体，在四周内生成约 600 万行 Lean 证明，验证了 Signal 已部署实现中的关键安全性质。

值得读的地方，是验证对象从简化模型走向了实际实现。但「若干性质通过机器检查」和「整个应用绝对安全」之间，还有边界需要讲清。

600 万行证明，究竟证明了什么

按原文描述，AlphaProof Code 是一个多大模型智能体框架：它把复杂的验证任务拆给多个智能体，由 Gemini 驱动它们生成证明，并借助 Lean 检查证明步骤。

Lean 是证明助手。可以把它理解成一个要求极其严格的检查器：你先写出前提、定义和要证明的结论，再提交推导过程，它负责检查这些推导是否符合规则。

这里有两种角色：AI 负责寻找和编写证明，Lean 负责检查提交的证明是否成立。模型生成了多少内容，不是可信度的依据；证明能否通过检查才是关键。

原文称，DeepMind 在 11 月 10 日的公告中披露了这项成果，整个过程耗时四周，产出约 600 万行 Lean 证明，并将其称为 AI 首次对广泛部署的加密协议完成形式化验证。

不过，报道没有列出「关键安全性质」具体有哪些，也没有解释攻击者能力、运行环境等前提。因此，我们能转述它声称完成了什么，却不能仅凭这篇报道确定证明覆盖了哪些攻击。

为什么验证实际实现，比验证模型更有分量

原文反复强调，目标是 Signal 已部署的协议实现，而不是简化模型。

这个区别很实际。协议模型描述的是设计应该怎样工作，用户运行的代码还包含具体的数据表示、状态变化和执行路径。设计成立，并不自动保证实现没有偏差。把验证落到实际实现，才能让结论更贴近用户正在使用的软件。

Signal 的协议保护着数百万人的消息，因此它也是一个具有现实分量的验证对象。原文还提到，这则消息在 11 月 10 日登上了 Hacker News 首页。

测试与形式化验证的区别，也应放在这里理解：测试检查选定输入下的行为；形式化证明则在明确的定义和前提下，证明某个结论成立。

形式化验证的覆盖范围，取决于写下来的命题和假设。

原文用「没有一步被遗漏」来强调证明的严密性，但这不能延伸成「没有任何安全问题」。没有被纳入命题的问题，无法靠这份证明顺带解决。

四周完成验证，能说明审计成本下降了吗

作者最看重的是时间：过去可能需要专家投入数年的大规模证明，如今由智能体在四周内完成。如果这个流程可以复用，验证工作确实可能变得更容易开展，也可能更频繁。

但这里要分清成果和推断。

四周、约 600 万行证明，是原文报告的项目结果；「审计成本将快速下降」，是作者据此作出的判断。报道没有提供算力开销、人工投入、前期准备时间，也没有给出同一任务由传统团队完成的对照数据。四周的日历时间，还不能直接换算成一般团队的采用成本。

原文称，DeepMind 已开源证明产物并发布技术论文。这比证明行数更有助于后续评估，因为其他研究者可以检查证明内容和适用边界。不过，所给文本没有附上相关入口，也没有展开复现条件。

文末提到的 1024-bit RSA 两个弱点，以及 Google 面向智能体 AI 开发 TPU 芯片，属于相关动态，不能用来补足这次 Signal 验证的证据。

我的判断

我认同这篇报道关注实际实现的方向。对于加密协议，能把明确的安全性质交给机器检查，比单纯展示模型解题能力更有工程价值。

需要打问号的是，它把「特定项目取得成果」推向「安全审计成本大幅下降」的速度有些快。缺少资源投入和对照数据，这部分仍是经验判断。

和常见的测试、人工审计相比，形式化验证提供的是另一类证据：测试帮助发现具体失败，人工审计帮助识别设计和实现中的风险，证明则回答明确命题在给定前提下是否成立。它们各有用途。原文也没有说明这套流程如何接入一般团队的开发与维护工作。

能拿来做什么

• 阅读类似的 AI 安全成果时，先找具体证明了哪些性质、依赖哪些假设、对应哪个实现版本，再判断结论与你使用的软件有什么关系。
• 如果团队维护加密协议实现，可以把这项工作作为评估 AI 辅助验证的案例，重点检查证明产物、复现条件和人工投入，别只比较完成时间。
• 在日常 AI 编程中，可以借鉴它的分工思路：让模型生成候选结果，再交给独立检查机制验证；涉及安全结论时，还要明确检查机制究竟覆盖了什么。