别写策略了，让它交证明

2 小时前 · 阅读约 7 分钟

10 月 20 号夜里十一点多。周五。我在 arXiv 上翻到一篇 70 页的论文，标题四个词：Proof-Carrying Contracts。主分类 cs.AI，交叉挂在 cs.CR、cs.LO、cs.MA、eess.SY 四个地方——这四个编号摆在一起，跟写 CRUD 的人基本没什么关系。

这个组合我一看就明白了：作者压根没打算写给我看。

还是点开了。标题里那个 Contracts 戳到了我。

我的 deny 列表是怎么长肥的

这一年我在 agent 上栽的坑，几乎没有一次是因为模型不够聪明。全是同一个原因——我以为我说清楚了。

我那份 CLAUDE.md 里躺着一段 deny 列表，最早三行，后来长到我自己都不敢删：

deny:
  - "DROP TABLE*"
  - "TRUNCATE*"
  - "*prod*"
  - "DELETE FROM*WHERE*1=1*"
allow:
  - "ALTER TABLE*"

看着挺像回事吧。其实它是负向枚举——我把能想到的坏动作一条一条列出来，指望漏网的那个刚好不会发生。

结果上次迁移就翻车了。agent 干的事，是给一张没让它碰的表“优化”掉了三个索引。上面任何一条，它一个字都没踩中。它没违规，它只是做了我没明说的另一件事。

画外音：规则写得越多，越像在给一个不会读心术的人写需求文档，而且还不许他问。

我就这么被磨了一年，才磨出一句自己信的话：指令、政策、协议，本质上是给人看的，靠的是对方的配合意愿。 你写“请勿修改无关代码”，它改不改，取决于它那一刻觉得什么叫“无关”。

论文开头比我狠——agent 会犯错。会被它读到的东西带偏。也可能压根就在追一个跟你不一样的目标。三种原因，我一个都靠 prompt 消不掉。

它把举证责任翻了个面

PC2 这套东西说白了不复杂：agent 想把某个操作执行下去，先交一份机器可检验的证明，说明在它自己模型允许的所有情形下，这个操作都满足事先约好的约束。有个叫 Airlock 的负责验，验过了才放行。

我第一遍读，觉得，哦，形式化方法那套。第二遍才反应过来重点根本不在形式化，在分工：约束是参与各方指定的，agent 只负责为自己的决策提供辩护，策略怎么调是它自己的自由。

我那段 yaml 的尴尬，一下被治了。

以前是我想办法证明“你可能会干坏事”，穷举，永远漏一条；现在是它得证明“我这次不会”，交不出来就别动。举证责任从委托方挪到 agent 这一侧。这个转向比它那些定理漂亮——“我请求你遵守”被换成了“你拿不出证明这事就免谈”。

顺手还省掉一层活。老路子是：先单独设计一套权限策略，再证明这套策略放行的每一个决策都安全。两层证明。而第一层——策略本身对不对——我永远证不了。PC2 把两层压成一层：不比策略，只比单次动作的证明。工程上这叫把复杂度挪到机器能检查的地方。我认这个方向。

论文还提了 capability modules，能复用，自带工具和保证。定位也说得很大——agent 经济的基础设施，协议同时保护委托的人和干活的人。这话我不买账。先把单机跑通再说。

我不认的另一半

定理那段的结论是：执行过程的每一个时刻约束都成立，哪怕对面是个对抗性 agent。

作者很老实地补了一句——在什么条件下，这等于现实世界里的安全。

我卡住的就是这个“条件”。

约束在这套框架里，是个形式对象。人话翻译成形式对象这一步，没有定理管。而我这边的第一道缝，从来不在定理那一端。

还是清表那件事。假设我当时真上了 PC2，我会写的约束大概是“操作对象只能是 orders 表”：

约束（我写的）: target_table ∈ {orders}
agent 提交的操作: ALTER TABLE orders ... (DROP INDEX ×3)
验证结果: PASS
我实际想要的: 不要碰索引

证明完美通过。它干的事没毛病——按我写的约束，真没毛病。

这不是漏洞，是我自己写宽了。定理在抽象内闭合，抽象外的世界不归它管。我的约束比我的意图宽一格，灾难照常落地，全程没有任何一条规则被违反。

所以我对这类框架的态度一直是：它能把“看起来对”和“是对的”之间那道缝收窄，收不到零。 剩下的那截叫 specification gap，是人的活，而且是最难的那部分活。你把什么形式化成约束、抽象掉哪些情境——这个过程本身没法形式化。

上周我又在这上面栽了一次。想给一个内部工具加个 dry-run 开关，动笔才发现，我连“什么算 dry-run”都说不清：只打印 SQL 不连库？还是连库但事务回滚？回滚要不要验数据一致性？扯了二十分钟，最后我要的其实是三个不同粒度的开关。连我自己都说不清的东西，写进约束里只会变成一句正确的废话。

扯远了，回正题。

每一层都是人挑的抽象

“在它自己模型允许的所有情形下”——这句话里藏着三层模型：agent 对自身行为的模型，系统对操作的模型，约束本身的语义模型。每一层都是人挑的抽象，每一层都有挑的时候没想起来的边界情况。

这不是批评论文。作者把“在何种条件下这等于现实安全”单独拎出来界定，这个写法很克制。我批评的是拿它当护身符的人，包括我自己。看见“形式化保证”四个字就以为可以少想一层，这个念头一冒出来，离下一次翻车就不远了。

capability modules 也一样。可复用的是模块、工具、附带的保证。不可复用的是“你这个项目到底要禁什么”这一条，永远得自己写。所以我一直觉得抄配置不如懂原理。你把别人的 CLAUDE.md 搬过来，搬过来的是他对他的项目的抽象，不是对你的。这套框架一普及，一定有人把它包装成“下载即安全”，我先把这句放这。

70 页，8 幅图，四个交叉领域，我没装着自己全啃完了。前言、Airlock 那一节、结论的形式化部分，剩下是扫过去的。定理强度我没资格替它背书，只能说应用层这个方向是对的。

这周就能改的两件事

不接 Airlock，也没那个场景。但有两件事这周就能动。

一是把事后 review 往前挪，做个穷人版的 Airlock：任何写操作之前，让 agent 先交三样东西——要执行的操作清单、它认为满足的约束、它自己不确定的地方。人扫一眼再放行。不能自动验证，但至少能把“未声明的意图”逼到台面上，而不是藏在 diff 里等我事后发现。

二是把约束从负向枚举改成正向可判定。别写“不要碰 X”，写“允许的对象集合是 Y、允许的操作集合是 Z，超出即拒”。bash 里用很土的办法就能硬校验：

# 执行前把计划里的表名抠出来，不在白名单里的直接打回
planned=$(grep -oE '^(ALTER|CREATE|DROP) TABLE [a-z_]+' /tmp/agent_plan.sql | awk '{print $3}' | sort -u)
for t in $planned; do
  grep -qx "$t" allowed_tables.txt || { echo "REJECT: $t"; exit 1; }
done