DeepMind 用智能体核验 Signal 协议代码

DeepMind 称，生成的 Lean 证明超过 600 万行。DeepMind 称，这是第一次对已广泛部署协议的实现做形式化验证。智能体把大约 1% 的范围标出供人复核，其余由 Lean 自动检查。全过程大约 4 周。

DeepMind 称，证明落到设备上实际运行的编译结果，其中包括设备一度失陷前后消息仍受保护。研究团队把两处已修复的真实缺陷放回隔离副本。两处都得到机器检查过的结论，带缺陷的版本不安全。DeepMind 称，验证材料将对外开放。

形式化证明要落到设备上正在跑的代码，难处在规格、证明和人工抽查三步都得接上，少一步就只剩设计层面的分析。数百万行证明靠多轮工具调用完成，开销在长上下文和反复推理，不在一次把训练卡跑满。国产加速卡若要承接这类任务，先得把 Lean 和长程智能体跑通，采购时不能只比单卡训练吞吐。