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.
This report is categorized under AITOP's "Models" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows and US-China foundation model benchmarks and commercialization comparison. Key entities and technical topics under continuous tracking include Google DeepMind, Gemini, Signal, Lean.
Source attribution: curated from rohanpaul_ai (@rohanpaul_ai).
