The keys of gatekeeper-not-driver are tokens, and their semantics independently reinvent two things:
- Petri nets (place / transition / token, OR-join; van der Aalst workflow nets) — reachability, deadlock, liveness all decidable. So a linter can statically warn "this deadlocks / this terminal is unreachable."
- Capability-based security (Dennis–Van Horn 1966; seL4) — a token is an unforgeable hold-grant. This sidesteps the no-MMU-in-attention problem (prompt-injection-is-buffer-overflow) by not putting power in the context: power is an object in harness state; the model can reference a token, never mint one.
Life-or-death line: minting authority lives with the verifier; tokens live in harness state, not in context text. The whole graph's strength = its weakest minting rule (deterministic check > human sign-off > model endorsement).
Sharpenings forced out in the dialogue: tokens should carry evidence (artifact hash + test report + signature); content-addressing binds a token to an artifact hash so re-edits auto-invalidate it ("the agent workflow's Bazel", and "keys go stale" = macaroon caveats / OCC validation). Consumable tokens → linear logic (Girard); loop fuel is a separate linear token → tdd-net-popper-mechanized.
Up: vibe-linter