DeepMind用AI代理验证Signal加密库 生成650万行证明
DeepMind称AlphaProof Code在四周内完成libsignal核心加密库的形式化验证，相关数学规范与证明已在GitHub开源。
据aitimes.com报道，DeepMind于2026年11月10日在其官方博客宣布，其多AI代理形式化验证系统AlphaProof Code完成了对Signal核心加密库libsignal的验证。整个过程中，AI代理在四周内编写了超过650万行数学证明代码。
据DeepMind介绍，此次验证覆盖Signal用于端到端加密的PQXDH握手与Triple Ratchet，证明保密性、身份认证、前向保密性以及入侵后安全性在编译后的机器码中依然成立。部分假设存在量子计算机攻击的安全属性，则在单独的数学模型中得到验证。
研究团队还将两个此前已修复的Signal漏洞重新植入代码，AlphaProof Code用数学方法证明两者均不满足安全条件。此外，需要人工额外审查的代码范围被缩小至总量的约1%左右。
Signal首席技术官Aaron Kretz表示，AI代理将形式化验证从有限范围大幅扩展到了实际实现代码。DeepMind已将验证所用的数学规范与证明在GitHub上以开源形式发布。
此次验证仅限于特定执行环境中编译的一对一消息加密代码，未覆盖群组消息与多设备状态。
相关研究背景
2026年11月6日，谷歌曾宣布AI在RSA加密中发现两处弱点，并发布可将加密密钥分解成本最多降低30倍的算法。同月早些时候，Anthropic发布了FlashProve，可通过密码学方式证明AI模型的回答来自特定模型。上月27日，開放人工智能与Anthropic分别发表了挑战计算复杂性领域一项长期假设的研究结果。
快速问答
AlphaProof Code验证了Signal的哪些内容？
验证覆盖Signal的PQXDH握手与Triple Ratchet，证明保密性、身份认证、前向保密性与入侵后安全性在编译后的机器码中成立；群组消息与多设备状态不在范围内。
DeepMind是否公开了证明代码？
是。DeepMind已将验证所用的数学规范与证明在GitHub上以开源形式发布。
这次验证用了多长时间？
AI代理在四周内编写了超过650万行数学证明代码。