快速了解本文
DeepMind 发布 AlphaProof Code 框架验证 Signal 核心库。
实现从 Rust 源码到 AArch64 机器代码的数学级安全证明。
人机协同四周编写约 650 万行 Lean 证明代码完成验证。
本摘要由 AI 辅助整理，请以正文内容为准。
数智朋克讯 2026年11月12日，Google DeepMind 发布 AI 形式化验证框架 AlphaProof Code，并成功将 Signal 加密协议核心库 libsignal 验证至编译后的机器代码级别。这是针对未修改的真实实现代码进行的数学级安全证明，消除了编译器引入漏洞的风险。
验证范围与技术细节
此次验证的源代码基础为基于 Rust 编写的 libsignal。研究人员将其连接至命令行测试程序，并编译为 AArch64 Linux 机器代码。验证覆盖了 Signal 协议的核心安全属性，包括 PQXDH（初始加密密钥协商）和 Triple Ratchet（消息交换期间的密钥更新），以及前向保密、消息认证和密钥泄露后的安全恢复条件。为验证框架的错误检测能力，团队将 2 个已修复的漏洞重新插入测试程序，成功在数学上证明了指定安全条件被违反。
人机协同工作流
在工作流上，5 名人类研究员与基于 Gemini Carbon 模型运行的 AI 代理合作 4 周，编写了约 650 万行 Lean 证明代码。人类专家负责审查和批准安全要求，AI 代理负责生成证明，最后由 Lean 验证器检查数学有效性。这种人机协同模式显著降低了复杂形式化验证的时间与人力门槛，但并非完全自动化，仍需人类专家把控安全要求。
目前，AlphaProof Code 仅针对特定架构和特定库完成验证，通用性仍有待观察。DeepMind 已公开相关的证明和代码，并建议该技术未来可用于验证医疗设备、电网等关键系统的安全性。