Google DeepMind这周公布了一个叫AlphaProof Code的系统，干了一件以前没人干成过的事：它用AI对Signal加密协议的实现做了形式化验证，而且是一直验证到编译后的代码这一层。按DeepMind的说法，这是第一次有AI把一个广泛部署的密码学协议验证到这个深度，也是第一次有任何方法做到实现级别的验证。代理们生成了600多万行Lean证明语言，花了4周时间，其中只有1%需要人工复核。验证过程中，系统还抓住了研究人员故意重新植入的真实漏洞。
理解这件事的关键，是区分”测一测”和”证一遍”。常规安全测试是抽查：跑一堆用例，没发现问题就放行。形式化验证是数学证明：它要证明在所有可能的情况下，某个安全属性都成立。过去这活贵得离谱，需要顶尖专家花几个月甚至几年手写证明，所以只用在最关键的系统上。AlphaProof Code把成本结构改了：机器写证明，人只复核1%。
验的不是论文，是跑起来的代码
以前的形式化验证大多停留在协议的数学模型上，证明的是”这个协议在纸面上是对的”。但纸面上的协议和实际跑的代码之间有巨大的缝隙：实现的时候一个边界条件写错，数学上完美的协议照样漏。AlphaProof Code直接对着Signal协议的实现下手，证明的是真实代码保持了”消息在设备被短暂入侵前后都受到保护”这类属性。
这也是它”第一次”的含金量：被验证的对象不是实验室里的玩具协议，而是几亿人每天在用的Signal。DeepMind还把验证产物开源了，等于给全行业递了一套新工具：以后审查一个加密库，不必只信作者的测试报告，可以直接看机器生成的证明。
从”测一测”到”证一遍”，安全范式在换
同一天还有另一条呼应的消息：OpenAI公开了Control Room，一个集中管理系统，登记每一个智能体研究工作负载的安全方案，一旦决定干预，能在35秒内叫停模型输出，而且系统本身出故障时默认停止输出。这两件事指向同一个趋势：AI安全的重心，正在从”发布前多测几轮”转向”运行中能证明、能叫停”。
对普通人来说，结论很实际：你用的聊天软件、银行App、智能设备，背后的安全审查正在从”人肉审计”变成”机器证明加人工复核”。成本下来之后，会有越来越多的关键软件被这样验一遍。但也要清醒：验证只能证明”被写进证明的属性成立”，没写进去的属性，它一个字都不会帮你查。
