AI 验证代码，正在从「跑一堆测试」变成「交一份机器可检查的数学证明」。11月10日，Google DeepMind 公布 AlphaProof Code，和 AI 智能体一起对 Signal 加密协议实现的关键安全性质做了形式化验证。小红书
工作分两步：先把 Signal 的安全目标写成约 2.6 万行 Lean 形式化规格与 AArch64 指令语义，人工逐条审核；再由智能体写出约 650 万行 Lean 证明，全部由 Lean 内核机器检查。论文写明，人类作者没有写任何证明代码。微博小红书
过去这类工作通常要专家团队花数年，这次前后约 4 周完成。微博
验证对象约 14 万条 AArch64 指令，覆盖后量子 PQXDH 握手和 Triple Ratchet，证明的是前向保密、认证、泄露后安全和握手保密。官方强调，工作不只停在协议设计，还涉及编译后代码与指定性质之间的对应关系。小红书小红书
报告还做了一次反向测试：把两个已修复的真实旧 bug 植回隔离版本，系统同样给出了这些版本不安全的机器检查证明。Signal 首席技术官称这是一次「重大突破」。微博小红书微博
这件事踩在 AI 编程当前的软肋上。JetBrains Research 今年 8 月发布的调查覆盖超过 1.5 万名专业开发者，今年 5 月至 7 月，全球约 90% 的专业开发者至少每周使用一次 AI 编程 Agent，68% 每天都在用。代码越来越多由 AI 写，社区里已经有人直言：人类不看代码，自然也不会去看测试，测试驱动在 AI 编程体系下变成了伪命题。Lean 创造者 Leonardo de Moura 的说法更直接：Lean 提供机器可检查的证明，你可以检查自己的证明，从而绝对确信它们是正确的。而形式化验证过去一直很贵，seL4 微内核的验证花了约 20 人年。36氪小红书小红书小红书
边界同样明确：只覆盖一对一会话，群聊、密钥生成、侧信道和多设备状态都不在范围内，底层密码原语的安全性作为假设。验的是团队封装的 libsignal-cli，不是 Signal App 本身，目前仍是研究项目，规格和证明已开源，等外界复核。微博小红书
论文里最值得琢磨的一句：证明变便宜之后，难的是「到底该证什么」。同一周，Anthropic 公布 Fable 5.2，官方自报的内部测试里，约 1000 个 Agent 协作、30 小时把费马大定理的证明完整形式化。费马大定理早已有人类证明，形式化做的是把推理写进严格的形式系统，让计算机逐步检查。对普通开发者，这件事的意义更多在工具层：AI 编程的竞争重点正在从「谁写得快」移向「谁能交出可验收的东西」，会写规格、判断哪些性质值得证明，正在成为人的位置。小红书小红书小红书
