一句话：这次真正变的不是 AI 会做数学题，而是它把人类从「写证明」这件事里解放了出来，只留下「写规格」这一件。
据 Google DeepMind 官方技术报告，AlphaProof Code 证明的是 Signal 协议参考实现 libsignal 的关键安全属性，而且是在机器码层面，直接对未经修改的 AArch64 二进制做验证。
翻译一下：以前说某个协议在数学上安全，通常只证明了纸面上的模型。这次被证明的，是真正跑在设备里的那段代码。
据 Wired 报道，Signal CTO Ehren Kret 的说法是，前人只验证过一小部分代码，DeepMind 这套方法把范围显著扩大了。
说白了，形式化验证就是给代码写合同
先把概念摁平。形式化验证做的事只有两步：给代码写一份合同，再证明这份代码在任何输入下都不违约。
合同里写的是「这段函数不许把密钥读出去」「这个状态机不允许两个会话共用同一个 nonce」这类话。证明则是让机器穷举逻辑上的所有可能，不是跑测试。
跟测试的差别就在这儿。测试是抽样，一千个用例全绿，也不代表第一千零一个不出事。证明是全称命题，一旦成立，这条属性就没有例外。
难的地方不在证明，在合同。合同写漏一条，机器证得再漂亮，也只是证明了你想说的那件事，不是你真正要的那件事。
卡在机器码这一层，因为跑起来的是二进制
协议层面的安全证明做了很多年。Dolev-Yao 那类符号模型把加密当黑盒子，只看消息怎么流、谁能看见谁。它能证明结构没问题，证明不了实现没问题。
编译器会优化，会展开循环，会重新排布内存访问。源码里那句检查，编到二进制里可能被挪了位置，甚至被判定成多余。协议证明管不到这一层。
据官方报告，AlphaProof Code 的做法是给 AArch64 机器码写一套形式化语义，然后直接对二进制做验证。省掉的正是「源码到编译器到二进制」这段信任跳跃。
这也是「首次」两个字的分量：把协议级的安全保证，接到一款被广泛使用的密码协议实现的未修改代码上。
650 万行怎么审：一队 agent 加一份留出规格
官方报告称，整个 Lean 开发约 650 万行。这个数字得这么读：它不是人一行行敲出来的证明，大部分是人在引导下由 agent 生成、再由 kernel 逐条核对的产物。
框架分三块。一是人引导的 agent 写 Lean 规格；二是 AArch64 机器码的形式化语义；三是一队自治的证明 agent。
划重点在这儿：证明 agent 交出的东西不算数，要过两道关。Lean kernel 检查通过，证明才算合法；Lean comparator 再确认它证明的恰好是事先留出来的那份规格，没有偷偷换题。
说白了，这是防「自证清白」。让 AI 自己出题自己答题，它很容易证一个更简单的命题然后宣布胜利。留出规格就是那把尺子。
把修过的 bug 塞回去，看它抓不抓得住
这套方法有个漂亮的自我校验实验：把 libsignal 历史上已经修好的两个 bug 重新注入进去。
结果是对照的。注入之后的二进制，Lean 证明显示它违反了符号安全定理。换句话说，规格不是摆设，它真能把错的东西判成错的。
这一步比证明本身更能说服人。证明通过只说明「没找到反例」，注入 bug 抓得住，才说明「找反例的能力是真的」。前者是沉默，后者是发声。
据 Wired 报道，对含已知旧漏洞的旧版本，AlphaProof Code 能识别出来并显示无法通过验证。DeepMind 同时表示，没在检查的部分发现新漏洞。
但这里有个前提
但这里有个前提：这套证明的可信度，最终仍压在几个假设上。
一，Lean kernel 本身得是对的。所有证明由它裁决，它错了，650 万行一起错。二，密码原语的安全假设得成立，计算模型下的证明也只是把攻击者的成功概率约束在某个界以下。
三，部分外部例程仍以 contract 的形式被信任，没有一路证到底。官方报告自己写了，大部分人类工作量已经从写证明转到了工程化规格上。
最要紧的一条：规格写错，照样白证。合同上写着「允许把密钥交出去」，代码老老实实照做，证明完美通过，安全性等于零。机器只保证一致，不保证你的意图是对的。
对写业务代码的人，先写契约再谈证明
全量形式化验证离普通业务代码很远，成本摆在那儿。但那套思路里有一半，今天就能用。
写接口的时候，把前条件和后条件写清楚：这个函数要求什么、保证什么、什么情况下会抛错。哪怕只是注释，也比没有强。
再往上一层，是把不变量显式写出来，比如「余额不允许为负」「同一个订单号只允许创建一次」。这些句子写出来，测试才知道该测什么，review 才有依据。
DeepMind 的做法顺序值得抄：先有人把规格写清楚，才有 agent 去证。反过来的顺序不成立。
门槛从写证明换成了写规格
回头看这次的事。它真正挪动的是人类在这一行里的站位：从证明的体力活里退出来，站到定义问题的那一端。
Signal 基金会过去的验证工作给了这套方法一个起步点，DeepMind 自己也承认这一点。前人铺的路没白铺，只是被接管了。
所以别急着问 AI 什么时候能替你写证明。更该问的是：你手头那套代码，合同写清楚了吗？
