AlphaProof Code 发布与 Signal 验证争议

第 1 集 · DeepMind AlphaProof Code 机器码级形式化验证 Signal 协议(2026-11-10,27 条)

11 月 10 日，Google DeepMind 发布多 LLM 智能体形式化规范与验证框架 AlphaProof Code，并宣布达成里程碑：在机器码层面对 Signal 密码协议（libsignal）的真实生产实现完成形式化验证，首次以任何方法（含 AI）数学证明了这一广泛部署加密协议实际代码的关键安全性质，验证历时约四周。次日 Sundar Pichai 公开宣布该成果，称 Gemini 4 Carbon 生成约 600 万行 Lean 证明完成了对 Signal 协议代码的数学证明。团队公开了论文与 Lean 证明代码，结论可由 Lean 机器校验，开源证明已受第三方核查。已确认

• AlphaProof Code 是用于深度形式化验证的多智能体框架，像研究团队一样分工协作，首个项目即针对 Signal 协议核心密码学代码；验证在机器码层面进行，覆盖实际编译代码（如 @markk 提到的 AArch64）而非仅协议设计
• 据 @swarat（DeepMind 团队成员）介绍，验证在约四周内完成，论文与 Lean 证明代码已公开，证明可机器校验
• @sundarpichai 宣布该成果由 Gemini 4 Carbon 完成，生成超过 600 万行 Lean 证明；@LuizaJarovsky 补充称 Lean 证明约 650 万行，整个过程在人类专家引导下进行；@javimbuilds 还提到人类仅审阅其中约 1%
• @kevrussell 转述称开源 Lean 证明约 750 万行，已受第三方核查；DeepMind 的 Pushmeet Kohli 称这是前沿软件验证的重要进展
• @rohanpaulai 概述了工作流：spec-writer agent 与用户协作把 Signal 的安全目标翻译成形式化数学规范，核心思路是「你永远不必信任 AI 本身」——证明由 Lean 在机器码级校验
• @jdluk87 指出形式化验证即用数学方法证明协议在所有条件下满足其安全声明，标准远高于传统渗透测试；同一协议也被 WhatsApp 和 Google Messages 采用

尚未确认

• 各帖对 Lean 证明行数的表述不完全一致（超 600 万、约 650 万、约 750 万行），可能对应统计口径不同，精确数字以官方论文为准

为什么重要

• 这是首次以任何方法（含 AI）对广泛部署的密码协议生产代码完成这种深度的形式化验证，@jedisct1 等安全社区人士视其为业界首次的重大突破
• 形式化验证此前成本极高、几乎不可能在合理时间内对生产密码代码完成，AI 智能体有望大幅降低这一门槛，且机器校验的证明不依赖对 AI 的信任；开源证明接受第三方核查进一步增强了可信度
• Signal 协议同时支撑 WhatsApp、Google Messages 等应用，每天保护数十亿条消息，验证结果的适用范围因此更广

• DeepMind 用 AI 一个月形式化验证 Signal 协议生产代码 — sebkrier · 2026-11-10
• DeepMind 发布 AlphaProof Code:四周形式化验证 Signal 密码代码 — TorturedPoet30 · 2026-11-10
• DeepMind 用 AI 数学证明 Signal 协议代码安全性，属业界首次 — jedisct1 · 2026-11-10
• DeepMind 用 AlphaProof Code 在机器码级形式化验证 Signal 协议 — swarat · 2026-11-10
• DeepMind 用 AlphaProof Code 在机器码级形式化验证 Signal 协议实现 — swarat · 2026-11-10
• DeepMind AlphaProof Code 4 周证明 Signal 编译代码安全，人类只审 1% — javimbuilds · 2026-11-10
• AI 证明 + Lean 机器码级校验:无需信任 AI 即可验证 Signal 安全性 — rohanpaul_ai · 2026-11-10
• AI 证明 + Lean 机器码级校验:无需信任 AI 即可验证 Signal 安全性 — rohanpaul_ai · 2026-11-10
• DeepMind 用 AlphaProof Code 机器码级验证 Signal 协议安全性 — LuizaJarovsky · 2026-11-11
• DeepMind AlphaProof Code 生成 650 万行 Lean 证明，首次完整验证 Signal 实现 — LuizaJarovsky · 2026-11-11
• Gemini 4 Carbon 用 600 万行 Lean 证明数学证明 Signal 协议代码 — sundarpichai · 2026-11-11
• DeepMind 详解 AlphaProof Code:多智能体分工形式化验证 Signal 协议 — sundarpichai · 2026-11-11
• DeepMind 用 AlphaProof Code 在机器码层形式化验证 Signal 协议 — tianyin_xu · 2026-11-11
• 爆料称 DeepMind 用 AI 形式化验证 Signal 代码，仅花四周 — IgorCarron · 2026-11-11
• DeepMind 形式化验证 Signal 协议机器码，开源 750 万行 Lean 证明遭第三方核查 — kevrussell · 2026-11-11
• DeepMind 用 AlphaProof Code 首次形式化验证 Signal 协议代码 — luislamb · 2026-11-11
• DeepMind 用智能体 AI 形式化验证 Signal 加密协议，被称里程碑 — jdluk87 · 2026-11-11
• DeepMind 用 AlphaProof Code 形式化验证 Signal 协议机器码 — kjgeras · 2026-11-11
• DeepMind 用 AI 智能体形式化验证 Signal 加密协议，属业内首次 — roydanroy · 2026-11-11
• DeepMind 用 AI 写 650 万行 Lean 证明，首次机器码级验证 Signal 安全性 — rohanpaul_ai · 2026-11-11

还有 7 条相关讨论 →

第 2 集 · MIT 教授 Tegmark 批 Wired 夸大：Signal 协议验证仅完成 80%(2026-11-12,2 条)

MIT 教授 Max Tegmark 就 Wired 对 Signal 协议形式化验证的报道提出批评，指其「夸大其词」。由他发起、与 Lean 定理证明器团队合作、Beneficial AI Foundation 主导的开源社区项目 SignalShot 实际只完成了约 80% 的验证。他借此提出「formal-washing」概念：仅因证明了部分性质就宣称系统安全，是一种洗白式包装，提醒公众警惕形式化验证成果的夸大宣传。

• Signal 形式化验证达 80%，MIT 教授称 Wired 报道夸大其词 — tegmark · 2026-11-12
• MIT 教授批「formal-washing」:Signal 协议验证只完成了一部分 — tegmark · 2026-11-12