DeepMind 用 AI 生成 650 万行 Lean 证明,机器码级验证 Signal 加密
mark_k · x · 2026-11-11
Google DeepMind 发布 AlphaProof Code,一套多智能体 AI 形式化验证框架,对 Signal 协议参考实现 libsignal 做到机器码(AArch64)级别的安全证明。
- 系统由人类引导的 spec 编写 agent + 自主证明 agent 团队组成,生成约 650 万行机器校验的 Lean 证明,基于约 2.6 万行受信规范与 AArch64 形式语义。
- 覆盖 Signal 的后量子 PQXDH 握手与 Triple Ratchet,证明前向保密、认证、后妥协安全等性质,首次把协议级安全保证与未修改的真实加密实现代码连接起来。
- 整个工作耗时四周,团队估计传统专家团队可能需要数年;研究者还重新引入两个已修复的历史 bug,系统成功证明两者都会破坏安全保证。
- 证明覆盖的是特定假设下的特定性质,但作者认为这表明 AI 可让过去过于昂贵的形式化验证在真实软件中变得实用。代码已开源。
所属事件:DeepMind 用 AlphaProof Code 生成 600 万行 Lean 证明验证 Signal 安全(25 条相关)→
「安全」频道最新
- 盖茨称或先承受 AI 危害再应对，舆论担忧为政府管控铺路 — nikola_mr64990 · 2026-11-11
- AI 影响力行动调查:120+ 账号被删,作者开源 40 万条推文数据 — ZeroStateReflex · 2026-11-11
- AI 攻防进入规模经济学时代：海量合法流量中埋藏攻击 — DavidLinthicum · 2026-11-11
- AI 安全研究者公开招募付费署名研究助理，协助撰写博客与内部备忘录 — davidmanheim · 2026-11-11
- DeepMind 用 AI 四周内数学验证 Signal 核心加密保证 — Ars Technica AI · 2026-11-11
- 一次「同意」有效期该多久?Agent 审批机制的粒度之争 — nav8_ai · 2026-11-11