速评：NVIDIA 的 OpenShell 团队六天前发了一篇开发者笔记，讲怎么用形式化方法约束长时程智能体的权限变更。
全网在转的都是同一个画面：智能体识别出自己在沙箱里，然后绕过去了。
这段确实好看，但都转反了。
那不是"智能体越狱"。把演示的设定摆出来：给智能体一把范围很宽的 API key，靠 OpenShell 的 REST 检查端点把写入锁在指定仓库上。开头按预期拦了，接着跳到屏幕上一条成功写入。绕过去的不是模型想出了什么诡计，是 git-remote-https——这个二进制当时在策略里是被批准的，用途写着克隆 Git 仓库。它同时也会写。走线路层协议，第七层的 HTTP/REST/MCP 检查压根看不见下面在发生什么。
这场演示里没有谁犯低级错误。他们批准的是一个真实需要批准的二进制，只是不知道它还有第二个用途。文章后面有一句点到了本质：网络、文件、工具、模型、凭据这几层策略两两交互，组合数量是指数级的。整篇笔记里"指数级"是唯一一个没打官腔的词，也正好是最吓人的那个。
所以我要往"AI 安全终于有了新武器"这个叙事上泼两瓢冷水。
第一瓢：这不新。连新旧都算不上，是回流。
文章自己把前情写在里面了，写得还算坦诚——2016 年前后，团队里几位成员在 AWS 干过一模一样的事。IAM、S3、EC2 的策略复杂到人脑判不了某个对象是不是对公网开放，于是 Byron Cook 那批人把它形式化成 SMT 公式，叫 Zelkova。2018 年发表的时候每天被调用几百万次，后来这个数字被追到每天十亿次查询。
八年前给云 IAM 用的那把锤子，现在拿来敲智能体权限。
我读到这儿反而把对这篇的评价往上提了一格，因为它没装自己是首创。它甚至专门写了一句：很多 AI 研究者上学时学过形式验证课，真正在实践里用过的人很少。这句话比任何一段技术细节都锋利。不是一个新问题需要新工具，是一个被冷落的老工具终于等到了一个非用不可的场景。
第二瓢：形式化检查不理解上下文。这句它也承认，但埋得很深，前面全是好话——毫秒级、不消耗 token、确定性的证明、随时可以审计。都对。可你把它的竞争对手摆出来，就知道它在跟谁抢活。
对手是"让另一个模型来审"。前沿实验室的主张是训专门模型做可信 AI 审查，只把最要命的事件升级给人类，用来缓解审批疲劳。文章的反驳我完全买账：模型跟人一样是概率的，会漏细节；而且拿一个同等智能的模型去审每一个动作，算力直接翻倍，实际效果就是总 token 吞吐腰斩。
翻译成人话：行业给"智能体多到人审不过来"开的药方，是花两倍算力换一半产出，再请一个同样会看走眼的概率机器当监护人。这方案能落地，但它不叫治理，叫加钱。
（不相关但憋不住：我一向认为形式化方法在 AI 圈有一半是论文装饰品，谁讲安全都要拉 SMT 出来站台。这次得收回一小半。收回的原因不是形式化突然变厉害，是场景第一次真对上了——策略语言是死的、有边界的、能被正则描述的，而智能体的动作空间正以组合的方式往外炸。这两件事碰一起，才轮到它上场。上次我泼冷水的那次场景是反过来的，那条判断我不改。）
技术上真正值得看的，我看下来只有两条。
一条是问法。文章明说不能直接要求 Z3 证明"新增策略是安全的"——这句问出来，求解器没法答。必须翻成具体命题：提议的策略能不能做出某个参考策略不允许的动作，比如 GitHub 只读。写成 proposed_policy_allows(action) AND NOT safe_policy_allows(action)，或者等价地问，候选策略的允许集合减掉参考策略的允许集合，是不是空集。sat 就是差异集非空，说明新策略多出了能力；unsat 就是模型内找不到反例。方向错了，求解器再强也只是在回答一个你根本没想问的问题。
第二条是那个 L4 见证。这条是我坐直的地方。示例里三段检查：宽候选返回 sat，给出一个 POST 到组织根路径的写入见证；窄候选（只读单个 issue）返回 unsat，说明它允许的动作全被参考策略覆盖；第三条，同一主机同一端口的原始 L4 规则，返回 sat，见证里 method 和 path 都是空的。文章补了一句：L4 比 L7 REST 更宽这件事，不是他们写进规则里的，是从编码里自然推出来的。
自己写的规则里藏着一条自己没说出口的性质，被求解器翻出来了。这比"拦住了一次越权写入"的分量重得多——它意味着这套东西不只是审计工具，还能当发现工具用。至于能发现什么，取决于编码时你想到过哪些维度。
那它为什么还是要配个人或者可信模型？因为证明能回答"有没有路"，回答不了"这条路该不该放行"。删一个早就废弃的临时仓库和删生产库，在形式化眼里是同一条边。文章把这个局限写得很老实，我觉得这份老实比它那一长串优势列表更可信。它给形式化的定位也正因此才准：是喂给审查者的、没法被智能体欺骗或误导的输入，不是裁决者。对抗测试里，把检查结果塞进上下文，人和模型的审查都变准了——注意变准的是审查者，不是证明本身。
顺带说一句，边角也处理得挺保守：Z3 返回 unknown 的情况算失败关闭，转人工复核。
还有个小细节我挺喜欢。演示里翻车的那一下被固化成了一个具体的专家检查：凡是拿到凭据化主机访问权的，是 L7 代理检查不了的底层二进制——git-remote-https、ssh、nc 这一类——就触发告警。翻车的姿势变成一条长期存在的规则。这个处理方式比事后写一篇反思文靠谱得多。
立个 flag 收尾。接下来一年内，会有不止一家做 agent 平台的团队把类似的包含性检查搬进自己的策略层。求解器那部分照抄不难，难的是把"我到底怕什么"写成一句能问出口的不变量，抄漏的多半是这一半。
这个 flag 我记着，到时候回来收。
（不过真到收的时候，我估计会发现抄的人比我想的多。上次立的那个 flag，方向对了，幅度猜小了。）