DeepMind 发布 AlphaProof Code：Gemini Carbon 智能体 4 周写出约 650 万行 Lean 证明，在机器码层面验证 Signal 协议实现的安全性

这件事意味着什么

【要点】

· 发布：Google DeepMind 于 2026-11-10 发布 AlphaProof Code，一个多智能体形式化验证框架，并附技术论文。

• · 成果：在机器码层面证明 Signal 协议参考实现 libsignal 的关键安全性质。
• 覆盖后量子 PQXDH 握手与 Triple Ratchet，证明了前向保密、认证、失陷后安全与握手保密。

• · 规模：智能体生成约 650 万行由 Lean 内核检查的证明。
• 可信基仅约 2.6 万行，包括规格与 AArch64 机器码语义。

• · 分工：人类专家与模型一起写 Lean 规格，每条都经人工审核
• 证明由 Gemini Carbon 驱动的智能体自动完成，只有约 1% 的代码需人工复看。

· 耗时：全程约 4 周。官方称同类工作以往需专家团队数年。

· 反向检验：把两个已修复的真实 bug 重新植入隔离副本，系统都给出了「该版本不安全」的机器可检证明。

· 开放：Lean 开发成果已开源。Signal CTO Ehren Kret 公开背书。

【我们的判断】

一

背景

· 形式化验证一直贵在人力：seL4 微内核验证用了约 20 人年，CompCert 约 6 人年，而且代码当初就是为验证而写的。

• · AlphaProof Code 验证的是未改动的生产代码经 rustc 编译后的机器码，不是协议设计。
• 这正是多数真实漏洞藏身的「设计与实现之间」。

二

对照

· Anthropic × Theorem（本站 e/1045）：在 RISC-V 汇编级为 123 个开源库证明「不崩溃」，约 1.8 亿行 Rocq，追求广度、性质较通用。

· AlphaProof Code：只做一个库，但证明的是密码学安全性质，追求深度。

· DeepMind 上周的 RSA 密码分析（e/1093）偏进攻侧；这次是防御侧的「证明无漏洞」。

三

影响

• · 这是 Gemini Carbon 少有的公开实战成绩。
• Carbon 目前仍只向部分网络防御方开放，尚无公开 API。

· 「AI 写证明、内核把关」的模式降低了对模型本身的信任要求，对医疗固件、电网等关键软件有直接意义。

· 要看的是可复现性：开源的证明能否被第三方独立检查与复用，以及框架是否开放给外部团队。

【可核验】

• · DeepMind 博文
• · 技术论文 PDF
• · Lean 开发成果
• · 本站相关：Anthropic×Theorem 汇编级验证（e/1045）；DeepMind 密码分析（e/1093）；Gemini 4 Carbon 发布（e/1063）