DeepMind 的 AlphaProof Code 验证 Signal 的加密核心

Google DeepMind 发布了 AlphaProof Code，这是一个能够以数学方式证明软件符合其安全规范的 AI 系统，并用它在四周内验证了运行在 Signal 用户设备上的加密核心代码，而这项工作通常需要数年时间。在专家定义了正式的安全要求后，基于 Gemini Carbon 构建的 AI 代理用 Lean 证明语言编写了超过六百万行代码，并标记出约百分之一的代码库供人工审查，立即发现了两个故意植入的漏洞。Signal CTO Ehren Kret 表示，随着 AI 威胁的增长，这种方法增强了对数据隐私的信任，DeepMind 计划通过 CodeMender 等系统将该方法扩展到电网和医疗设备。

据 Ars Technica 报道，Google DeepMind 完成了一个为期四周的项目，用数学方法验证了 Signal 的关键部分。这项工作暗示，AI 可能让形式化验证变得实用得多，不过报道没有提供更多技术细节。