|
Google DeepMind于11月10日介绍AlphaProof Code：一个由人类专家与AI代理协作的形式化验证框架。研究团队将它用于Signal协议参考实现libsignal的特定编译后机器码，尝试把协议层的安全目标对应到实际运行的代码。
工作流程中，专家先确定并审查要证明的形式化规格，之后由AI代理生成Lean证明，最终由Lean内核检查证明是否成立。DeepMind称，代理生成约650万行机器检查的Lean证明，覆盖Signal一对一会话中的部分安全性质，包括前向保密、认证、事后泄露安全和握手保密；团队还把两个已修复的真实缺陷重新引入隔离版本，证明系统能识别对应版本不满足规格。
这项结果的边界很重要：它不是对Signal整个应用或所有使用方式的全面安全认证。研究只覆盖明确建模的一对一协议范围和指定性质，不包括群聊等场景；证明也建立在研究人员审核的规格及模型假设上。它展示的是AI代理协助生成大型证明、再交由形式化证明内核核验的流程，不是让AI自行判断“软件绝对安全”。
来源：Google DeepMind官方研究公告（2026年11月10日）
https://deepmind.google/blog/introducing-alphaproof-code/
技术论文与证明工件：https://google-deepmind.github.io/code-verification/
代码：https://github.com/google-deepmind/code-verification |
0