Token：Petri 网 + capability（能力）

gatekeeper-not-driver 的关键在于 token，而 token 的语义不约而同地重新发明了两样东西：

• Petri 网（库所/变迁/token、OR-join；van der Aalst 的 workflow net）——可达性、死锁、活性都是可判定的。因此 linter 可以做静态检查，警告"这里会死锁 / 这个终态不可达"。
• 基于 capability 的安全模型（Dennis–Van Horn 1966；seL4）——一个 token 就是一份不可伪造的持有即授权凭证。这绕开了 attention 里没有 MMU 的问题（prompt-injection-is-buffer-overflow），办法是不把权力放进 context：权力是 harness state 里的一个对象，模型只能引用一个 token，永远不能铸造一个 token。

生死攸关的一条线：铸造权归属于 verifier；token 活在 harness state 里，不活在 context 文本里。整张图的强度，等于它最弱的铸造规则（确定性检查 > 人工签字 > 模型背书）。

对话中被逼出来的几处磨细：token 应当携带证据（artifact hash + 测试报告 + 签名）；content-addressing 把一个 token 绑定到某个 artifact hash 上，这样一旦重新编辑，token 就自动失效（可以叫它"agent workflow 版的 Bazel"，而"钥匙会过期"对应的正是 macaroon caveat / OCC 校验）。可消耗的 token 对应线性逻辑（linear logic，Girard）；loop 的燃料是一个独立的线性 token → tdd-net-popper-mechanized。

上级：vibe-linter