DeepMind称四周完成Signal密码核心验证

Google DeepMind 展示的 AlphaProof Code，尝试把 AI 编程推进到另一步：让 AI 为代码写出可检查的数学证明。按原文报道，他们用四周完成了 Signal 实际加密核心代码的验证，而这类工作通常需要数年。

值得看的是验证对象：此前的工作停留在理论设计，这次触及用户设备上运行的代码。不过，「满足已定义的安全要求」和「软件绝对没有漏洞」之间，仍有一段需要讲清楚的距离。

四周完成的，到底是哪一层验证

加密协议在理论上成立，不代表实现它的代码就一定正确。设计描述的是应该怎样运行，代码还要把这些要求落实到具体操作里。

原文称，AlphaProof Code 验证了 Signal 在用户设备上运行的实际加密核心代码。相比此前停留在理论设计阶段的验证，这一步更接近真实软件。

这里的形式化验证（formal verification），可以理解为：先把安全要求写成精确的数学命题，再证明程序满足这些命题。它与测试的区别在于，测试检查选出的输入和运行结果，形式化证明则试图在明确的前提下建立普遍成立的结论。

证明成立的范围，取决于安全要求写了什么。

因此，这次结果不能直接扩展为整个 Signal 应用都已验证，也不能据此认定所有潜在攻击方式都已覆盖。原文没有交代具体覆盖哪些安全性质、实现边界和运行环境。

AI 写了六百多万行证明，人仍要定义要求

这套流程并非把代码交给模型，再让模型回答「安全」。

按报道，专家先定义形式化安全要求；基于 Gemini Carbon 的 AI agents 随后使用 Lean 证明语言，编写了超过六百万行证明。系统会协助创建规格，再对程序是否满足规格进行独立证明。

Lean 在这里承担的是表达和检查数学证明的角色。六百多万行说明生成规模很大，但行数本身不是安全程度的评分，也不能直接换算成节省了多少人工。

系统将约 1% 的代码库标记为需要人工复核。原文没有说明这个比例的统计口径，也没有说明这些代码为何需要复核，不能据此推导出剩余部分完全不需要专家参与。

研究人员还故意植入了两个 bug，系统立即发现了它们。这是有价值的检验，但原文没有给出 bug 类型、难度和更多测试样本。它证明系统抓住了这两个问题，尚不足以描述完整的漏洞发现能力。

我的判断

我看好的是分工：专家负责明确「必须保证什么」，AI 承担大量证明构造工作。对于加密核心这类安全要求严格、人工证明成本高的代码，这条路线有明确价值。

但「四周代替数年」需要保留条件。原文给出了项目耗时和通常耗时，没有提供同一任务的人工对照，也没交代团队规模、算力成本，以及规格准备是否计入四周。它是一次成果展示，还不是一般团队可以直接套用的效率指标。

与常见的单元测试、模糊测试和代码审查相比，形式化验证能提供不同类型的保证，但也更依赖规格是否准确、覆盖是否充分。几种方法可以互补，不能仅凭这次报道判断谁能全面替代谁。

Signal CTO Ehren Kret 认为，这种方法有助于在 AI 威胁增长时增强用户对数据隐私的信任。DeepMind 还计划通过 CodeMender 等系统，把方法扩展到电网和医疗设备。前者是对价值的判断，后者是后续计划，都应与本次已经展示的验证结果分开看。

能拿来做什么

• 在日常 AI 编程中，先把关键约束写清楚，再要求 AI 实现。例如哪些状态不可出现、哪些输入必须拒绝，让审查有明确依据；这还不等于形式化验证，但能借鉴其工作顺序。
• 评估 AI 安全工具时，追问它验证的是协议设计、实际实现，还是有限测试样本，并要求说明覆盖范围与人工复核部分。
• 如果团队维护加密相关代码，可以关注这类工具能否用于边界明确的核心模块。原文没有提供可直接使用的 API、命令或接入方式，目前更适合作为技术路线参考。