AlphaProof Code 用 Lean 验证 Signal 加密核心

Google DeepMind 公布的 AlphaProof Code，试图把 AI 编程推进到另一层：由专家确定安全要求，让 AI 为实际运行的代码生成数学证明，再交给 Lean 检查。他们报告，用四周完成了 Signal 核心密码代码关键安全性质的形式化验证，并在两个历史缺陷的回放中证明了缺陷版本不安全。

值得读的地方，是这套工作流如何分配信任。模型负责承担繁重的证明工作，人负责审查规格，检查器负责验算。但它验证了哪些代码、依赖哪些假设，仍然决定着结论能覆盖多大范围。

为什么证明协议设计还不够

Signal 协议保护着 Signal、Google Messages 等应用中的数十亿次私密对话。对于这样的密码协议，算法设计正确，只是安全链条的一部分。

设计描述的是应当怎样工作，产品里运行的却是具体实现。代码可能偏离设计，编译后的执行行为也需要纳入考虑。原文强调，现实漏洞经常藏在设计与实现之间，而过去的大量协议验证停留在设计层。

AlphaProof Code 要跨过的就是这段距离。按作者的描述，他们证明了编译后的代码满足专家指定的关键安全性质，验证深入到设备实际运行的代码，并借助 Lean 中的处理器模型描述执行行为。

其中一个目标，是确认设备遭到暂时入侵前后的消息仍具备规定的保护。这里不能理解成「设备被控制也完全没事」：具体保护哪些消息、攻击者具有什么能力，要由形式化规格和假设共同界定，原文没有展开这些条件。

这次工作的价值，是把安全主张连接到实现代码，而不是只停留在协议设计。

作者称，这是首次利用 AI，以这样的深度验证广泛部署的密码协议；也称此前没有任何方法完成过同等深度的此类实现验证。这些是作者对研究位置的判断，所给材料没有提供完整的同类工作对照。

AI 写证明，谁来保证证明可信

AlphaProof Code 是一个多大语言模型智能体框架（multi-LLM agentic framework）。它把形式化验证拆成类似研究团队的协作流程，而不是让一个模型从头包办。

第一步是确定证明目标。研究人员与多种模型协作，把 Signal 的安全目标写成数学规格，再由人类专家逐一审查。规格就是能够被严格检查的安全要求：系统究竟要保证什么，哪些行为算违反要求。

第二步由 Gemini Carbon 驱动的智能体生成证明。作者报告，这个过程产出了超过六百万行 Lean。Lean 在这里既是表达规格和证明的语言，也是检查证明是否成立的工具。

第三步是检查与审计。Lean 自动检查证明，智能体还会审计证明产物，把需要人类复核的部分标出来。作者称，这部分仅占代码库的 1%，专家因此可以把精力集中到需要判断的位置。

这里最关键的安排，是把生成证明和接受证明分开。模型可以提出错误的推理，检查器必须按形式规则决定它能否通过。流程图也把证明团队标为不可信的一方，把最终检查环节放在信任边界上。

但检查器并不能代替人判断「这个要求是否值得证明」。假如规格漏掉了一种攻击，即使现有证明全部通过，也不会自动补上遗漏。

机器检查能确认推理符合形式规则，安全目标是否完整仍然需要专家负责。

四周和两个旧漏洞，分别证明了什么

作者报告，整个验证过程用了四周，而同类高难度工作在历史上往往需要专家团队投入数年。这展示了 AI 承担证明劳动的潜力。

不过，原文没有给出参与人数、模型调用量、算力成本，也没有列出相同范围的人工验证基准。因此，「四周」是这次项目的结果，不能直接换算成普通团队可复现的效率倍数。

六百万行 Lean 同样需要放在这个语境里理解。它说明生成产物规模很大，但行数不等于覆盖了多少安全风险，也不能单独证明验证质量。

作者还做了一项更有针对性的检查：在隔离版本中重新引入两个真实存在、此前已经修复的 Signal 漏洞。两次实验中，系统都生成了经过机器检查的证明，表明缺陷版本不安全。

这比只报告「正确版本通过了」多了一层证据：系统能够在这两个具体案例中区分安全性质是否成立。但它仍不是未知漏洞发现能力的全面评估。原文没有说明系统是否提前知道缺陷位置，也没有提供更多样本或失败案例。

所以，这组实验支持的是有限而明确的结论：针对选定的安全性质和两个历史缺陷，系统给出了可检查的结果。它不能推出系统可以自动找出任意漏洞。

我的判断

我认可这条路线。让 AI 生成可由独立工具检查的产物，比只让模型读代码、给出「看起来安全」的评语，更适合承担严格的安全保证。模型的输出不再只是供人参考的文字，而是必须经过规则检验的证明。

和单元测试、模糊测试相比，形式化验证能够在明确假设下证明某类性质，对密码协议这样的对象尤其有价值。但这些方法解决的问题不同：测试可以帮助发现规格之外的异常，形式化证明则取决于规格、模型与实际实现之间的对应关系。

这篇公告最需要保留问号的是验证边界。它没有列出精确的代码版本、覆盖模块、处理器模型假设，以及外部依赖如何处理。没有这些细节，就不宜把「核心密码代码的关键性质得到验证」扩大成「整个 Signal 应用不存在安全漏洞」。

「只需人工复核 1%」也不能直接变成项目预算。原文没有明确这个比例的统计口径，更没有证明那 1% 的审查很容易。确定规格、理解攻击模型，仍可能需要稀缺的专家投入。

模型信息也要分清：正文写的是 Gemini Carbon，文末关联文章标题出现 Gemini 4 Carbon，两者关系没有解释，不能自行认定为同一版本。

作者称将开源验证产物，但输入材料没有提供可核查的产物清单。至于进一步用于医疗设备固件、电网软件，以及与 CodeMender 配合防御网络攻击，目前属于研究方向。作者也明确承认，扩大应用规模仍需要继续研究。

能拿来做什么

• 在日常 AI 编程中，先写清楚必须成立的性质，再让模型修改实现。例如 Node 服务中的权限判断，要明确哪些身份可以执行哪些操作，并为这些要求配置独立检查；这借鉴了规格先行的流程，不代表已经完成形式化验证。
• 对已有的 AI 代码审查流程，加入历史缺陷回放。像作者重新引入两个已修复漏洞那样，检查工具能否识别已知错误，比只观察正常代码能否通过更有判断价值。
• 如果团队维护密码协议或其他高价值安全模块，可以评估一个边界明确的验证试点。先确定目标代码、环境假设和安全性质，再讨论是否投入形式化工具；这篇公告不足以支持一次性验证整个应用。
• 评估 AI 验证方案时，要求提供规格、覆盖范围和机器检查产物。四周、六百万行、1% 都值得关注，但真正决定能否采用的，是这些结果具体保证了什么。