Google DeepMind 使用 AlphaProof Code 验证 Signal 协议代码

发生了什么

Google DeepMind 的研究人员使用 AlphaProof Code，对 Signal 协议底层编译代码的关键安全属性进行了形式化验证。这个多 LLM 框架生成了超过六百万行 Lean 证明，并由 Lean 自动检查；人类专家审查了每项规约，并重点复查了被标记为需要再次审查的百分之一代码库。整个过程耗时四周；针对两个此前已修复漏洞的测试生成了机器检查的证明，证实存在漏洞的版本并不安全。

接下来读什么

• 今日还有哪些重要变化Google DeepMind 推出 Gemini 4 Hydrogen，加速智能体工作流

5 家信源报道

这件事到目前为止

Google DeepMind 使用 AlphaProof Code，对 Signal 协议底层编译代码中的部分密码学保证进行了形式化验证。这项为期四周的概念验证生成了超过 600 万行 Lean 证明，均由 Lean 自动检查；人类专家审查了每项规范，并检查了约占代码库 1% 的、被标记为需要再次审查的代码。检查的部分未发现新的漏洞。 使用两个此前已修复的漏洞进行的测试，生成了机器检查的证明，表明较早的含漏洞版本并不安全。DeepMind 正在发布其规范和证明，以支持进一步的形式化验证工作。