DeepMind 用 AI 写 650 万行 Lean 证明，首次机器码级验证 Signal 安全性
rohanpaul_ai · x · 2026-11-11
Google DeepMind 发布 AlphaProof Code，一个多智能体形式化验证框架，对 Signal 协议参考实现 libsignal 在机器码层面完成安全属性证明。
- AI agent 生成了约 650 万行经机器检查的 Lean 证明代码，基于约 2.6 万行可信规范与 AArch64 形式化语义；证明仅当 Lean kernel 校验通过才被接受，连 Rust 编译器也不被信任。
- 证明覆盖 Signal 的后量子 PQXDH 握手与 Triple Ratchet，确立了前向保密、认证、后妥协安全与握手保密。
- 这是首次有方法（无论是否用 AI）对广泛部署协议的真实生产代码做这种深度的形式化验证，把协议级安全保证一直连到处理器实际执行的指令层面。
- 团队认为这表明 AI 能让历史上过于昂贵的形式化验证在真实系统中变得实用。Lean 开发已开源在 google-deepmind.github.io/code-verification。
所属事件:DeepMind AlphaProof Code 机器码级形式化验证 Signal 协议(27 条相关)→
「安全」频道最新
- AI 安全研究者 Andrew Critch：别把灭绝风险称作「自我改进」 — AndrewCritchPhD · 2026-11-12
- 美分析：任一州可借 Parker 豁免使 AI 安全协作合法化 — TinfoilTricorn · 2026-11-12
- 芝加哥学区全线封禁学生用 ChatGPT/Gemini，引隐私法规为由 — lmoroney · 2026-11-12
- AI Horizons 论坛 12 月旧金山办会，千人规模共建 AI 安全生态 — austinc3301 · 2026-11-12
- 讨论：探针系统已是 OpenAI 监控体系的第一道防线 — dfrsrchtwts · 2026-11-12
- Kaspersky 披露 Black Owl APT 渗透软件商基础设施图谋供应链攻击 — cyb3rops · 2026-11-12