Google DeepMind 用 AI 数学证明 Signal 代码安全性
Google DeepMind 用几十个 Gemini Carbon 智能体写了 650 万行 Lean 证明，4 周干完过去专家团队几年的活，还故意塞回 2 个旧漏洞验证系统真能抓出问题。做安全、写关键系统的工程师都该看看这个验证思路。
Google DeepMind 宣布用 AI 智能体对 Signal 的真实运行代码完成数学级安全证明，生成约 650 万行 Lean 证明代码，验证对象直达处理器实际执行的指令级别。该团队表示此前从未有人对任何广泛使用的协议做到这一点。
技术上，团队使用 40 到 80 个 Gemini Carbon 智能体撰写 Lean 证明，Lean 证明检查器会拒绝任何错误步骤，因此无需信任 AI 本身。人类负责设定安全目标并审查智能体标记的约 1% 内容。由于 Rust 编译器也不在信任范围内，编译器引入的错误同样会被证明捕捉，从而填补设计与代码之间的缝隙。
整个验证耗时 4 周，而过去专家团队通常需要数年。为排除系统只会通过任何代码的可能，研究者将 2 个已修复的旧 Signal 漏洞重新植入副本，两次都得到机器检查的证明指出代码不安全。随着成本大幅下降，这类机器验证证明有望成为固件、电网软件等关键代码的常规检查手段。
Big achievement by Google DeepMind for showing that an AI system that proves a software is secure mathematically, with no need to trust the AI.
> They just used AI agents to mathematically prove that Signal’s real running code keeps messages secret.
Google's AI agents wrote 6.5M lines of math proving Signal’s compiled code keeps chats private.
checked at the level of the instructions a processor actually runs. The lab says no one had done this before for any widely used protocol.
> Normal testing tries many inputs and hopes to hit the bad one. A proof shows the security rules hold in every case, and the Lean proof checker rejects any wrong step the AI writes.
> Real bugs often creep in when a design gets turned into code, so checking the processor-level code closes that gap. The Rust compiler isn’t trusted either, so a mistake by the compiler would also get caught.
> The work took 4 weeks, where expert teams used to need years. Teams of 40 to 80 Gemini Carbon agents wrote about 6.5M lines of Lean, while humans set the security goals and reviewed the 1% the agents flagged.
> To check that the system can’t just approve any code, the researchers put 2 old, already fixed Signal bugs back into a copy. Both times it produced a machine-checked proof that the code was insecure.
> The bigger shift is cost, now that AI can produce machine-checked proofs in weeks, rather than years-long projects and become routine checks for device firmware, power grid software and other critical code.
本条情报归属 AITOP「模型」核心栏目，重点聚焦北美前沿实验室与硅谷科技巨头。在跨区域产业观察坐标中，该动态直接关联「AI 开发者工具链、Coding Agent 与工程化实践」「中美大模型技术代差与商业化对照」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：Google DeepMind、Gemini、Signal、Lean，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始线索采编自「rohanpaul_ai」（@rohanpaul_ai），经 AITOP 多维评分管线结构化提炼。
