ARTICLE · 1342318
我用了八年的加密 App,被一群 AI 用了四周证了一遍
我用了八年的加密 App，被一群 AI 用了四周证了一遍
我用 Signal 八年，一直只信它设计上安全。DeepMind 用 AI 智能体生成 600 万行数学证明，把跑在几十亿人手机上的真实代码证了一遍。安全，第一次从承诺变成可算的题。
1️⃣八年了，我只信它设计上安全
我是对隐私有点执拗的人。Signal 在我手机里装了八年，理由很朴素，它的端到端加密设计是公开的，全世界密码学家都能来挑刺。可设计安全和代码真的安全中间，隔着一条很深的沟。设计是一份蓝图，代码才是盖起来的楼，蓝图挑不出毛病，不等于施工没留缝。代码是人写的，人总会在设计与实现之间留下缝隙，有些漏洞偏偏只长在蓝图变成砖块之后。要填这条沟，过去得请一队专家花好几年一行行审。我从没指望过这件事真的发生，因为它贵，也因为它慢。
2️⃣DeepMind 这次，把事实摆上了桌
11 月 10 日，Google DeepMind 说他们用一套叫 AlphaProof Code 的框架，把跑在 Signal 里的真实代码用数学方法证了一遍。不是证那张纸上的协议，是证你手机上那段编译好的代码。Lean 是一种专门让机器核对数学证明的语言，人读着累，机器却一眼能看穿哪里站不住。智能体生成了超过 600 万行 Lean 写出的证明，AI 审完剩下 1% 交给人，其余由机器自动核对，不留情面。他们要证的也不是边角功能，而是最要命的一条：设备被短暂攻破前后，你的消息依然守得住。整个过程花了四周。同样的事，过去一队专家要干好几年。
3️⃣最狠的一招，是它自己抓到了 bug
为了证明这套方法不是花架子，研究者干了一件很聪明的事。他们把两个早就修好的真实漏洞，重新塞回隔离版本里。结果系统在两种情况都给出了机器可验证的证明，说明那段代码确实不安全。等于说，这个 AI 审计员不只会背书，还会抓人。Signal 的 CTO Ehren Kret 说，这把形式化验证的范围推得更广，也让人对隐私保护更有底气。
4️⃣但四周，不等于万事大吉
我得把话说回来。DeepMind 自己承认，要把这套技术铺到医疗固件、电网软件上，还得做更多研究。四周是个起点，不是终点。而且开源的那份验证产物是给社区复查用的，普通用户看不见也读不懂，它保护的是 Google Messages 里几十亿条对话底下的那层信任，不是你的聊天记录本身。我的安全感多了三分，但没满。加密世界从来不是赢一次就结束的游戏，今天证过的代码，明天可能被新写法重新打开。
🧠 波波池怎么看
我觉得这件事最被低估的地方，不在 AI 会证明代码本身，而在它把可信的门槛从人证变成了机证。过去我们信一个加密 App，靠的是专家背书和大公司信誉；现在 DeepMind 给了一份可被任何人复算的数学证据，且不依赖你信不信。更关键的是它开源了验证产物，意味着谁能证明不再是实验室的专利。我的判断：形式化验证会从实验室奢侈品变成软件的强制标配，就像当年的代码审计。下一个被盯上的可能不是聊天软件，而是那些一旦出错就会死人的系统，心脏起搏器、电网、自动驾驶。AI 在这里真正的价值，是把安全从一句承诺变成一道能算的题。
💬 你愿意为了被数学证明过的安全，换用一个操作更麻烦的 App 吗？
评论区见 👇
波波池 · AI赋能设计与前沿交互黑科技
原创内容，转载需授权 · 2026-11-11
