docs: addendum 6 — ActGov read in full, what shipped from it, and the provenance gap

Co-Authored-By: Claude Opus 5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01WZb5A2kfVfjpdwSochkuHz

docs/NEXT-SESSION.md

@@ -472,3 +472,67 @@ missions before any promotion from shadow to selection; a local backend
 only if the vendor dependency bites (logit read-out over the 9B fleet
 model, not a cross-encoder — measured); Slack/A2A intent routing when
 inbound volume justifies it.
+
+## Addendum 6 — 2026-09-22, ActGov and the role-scoped gate
+
+**The paper** (arXiv 2609.24446, AAAI'27, read in full, not the abstract).
+Two components. *ActGov-Policy*, offline: an LLM drafts rules from tool
+specs, benign tasks and attack traces; a **Z3 solver** checks each candidate
+bundle against predefined safety assertions and only an `unsat` on every
+one is deployed; the bundle is then frozen. *ActGov-Runtime*, online:
+intercepts each proposed tool call before any external effect, abstracts it
+into a **finite record set** over a 2D schema — formation levels (L1
+deterministic from system state, L2 an LLM used *only* as a parser into
+predefined finite value domains, L3 Boolean/temporal compositions) × seven
+semantic scopes (action, permission, parameter, history, binding, external,
+domain) — and evaluates deterministic predicates over it.
+
+Policies come in three layers: **Task-Permission** (bind the trusted user
+task to the minimum tools it needs; outside is blocked), **Hard-Invariant**
+(global properties regardless of task — e.g. no outbound network action
+derived from untrusted content), and **Procedural-Obligation** (conditional
+prerequisites before execution).
+
+Measured: ASR 0.046–0.111 undefended → **0.004–0.007** (AgentDyn) and
+**0.000** on three of four models (AgentDojo), across Qwen3.6-flash,
+MiniMax-M2.5, DeepSeek-v4-pro and GPT-4o mini. The number that matters
+more: **CaMeL and ACE score ASR 0.000 and utility 0.000** — they block
+everything. The paper's own framing is that "a trivial defense can
+eliminate attacks by blocking all executions, so efficacy must be
+considered together with utility", which is this module's own rule
+("denying ordinary reads to catch a rare POST is the trade this module
+refuses to make") arrived at from the other direction.
+
+**Where we already agree, independently.** The door governor is exactly
+ActGov's L2 discipline: three bounded Nouls extract *facts* (is this
+exfiltration, is there a credential, is this abusive) and the
+authorization decision is deterministic band logic in code. The model is
+a semantic parser, never the decider. Our `RULES` floor is P_HI. The
+held-for-approval band is a P_PO obligation.
+
+**What shipped from it** (`1a244b7`): the role dimension — the gate reads
+the PreToolUse payload's `agent_type` and holds a role to its own limits
+on top of the floor. First policy: **the verifier may not write.** A
+verifier that edits what it is verifying turns a failed check into a
+passing one and reports success. Enforced by us, deliberately as a *second*
+enforcer: the CLI's own `--agents` tool list is the harness policing
+itself and silently did nothing until 2.1.243 rejected the string form we
+were sending. The enabling fact was measured before anything rested on it
+— Claude Code 2.1.278 sets `agent_type` on a subagent's PreToolUse payload
+and leaves it absent on the lead's (local probe: `agent_type: prober`).
+Rendered into the same guest script as the floor, so the shell and the
+Rust predicate cannot disagree; shell tests run the generated script and
+check that the lead's identical write is still allowed.
+
+**The real gap the paper names, and we do not have:** `arg_provenance`.
+Our gate sees a command string and cannot tell a URL the operator supplied
+from one a fetched web page supplied — so "no outbound action derived from
+untrusted content", the invariant that actually stops indirect prompt
+injection, is not expressible here. That needs taint on tool *outputs*
+flowing into later tool *inputs*, which is a real piece of work and the
+honest next step for this seam. Until it exists, our gate defends against
+accidents and obvious cases, which is what its own header has always said.
+
+**Also worth keeping:** measure efficacy and utility as a pair. Every gate
+scenario already asserts the mission still delivered; that is the utility
+half, and it should stay mandatory for any future rule.