Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives¶

🕒 Published (v1): 2026-07-15 05:55 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

Six widely used open-source LLM agent frameworks (LangGraph, LlamaIndex Workflows, Microsoft Agent Framework, OpenAI Agents SDK, CrewAI, LangGraph.js) ship HITL approval gates, cancellation, and timeout primitives that imply barrier semantics but fail to enforce them. The central failure, called the sibling leak, lets a concurrently executing branch commit an irreversible side effect while the run is paused awaiting human approval—making rejection powerless. SOUNDGATE, a formally verified, environment-external Rust gate, repairs all four violation classes across all six frameworks at ~1 ms per write and ~12k admissions/second.

Problem¶

Agent frameworks expose control primitives (approval gates, cancellation, timeouts) whose names and documentation imply a barrier contract (B1–B4): no gated effect executes during a pause; rejection prevents the effect; each effect executes at most once; cancellation/timeout stop in-flight effects. This contract holds on none of the evaluated frameworks. The gap is not one implementation's bug—it recurs across four independent execution models (Pregel/BSP supersteps, event bus, message-passing fan-out, parallel tool calls) and two language runtimes—yet has not been characterized or repaired at a framework-independent level.

Method¶

Measurement (C1): Model-free differential probes instantiate minimal workflows where the control primitive under test is the only varying factor; side effects are in-process event-log appends instrumented at the commit point. Each probe has a pre-registered binary violation predicate (B1–B4). No LLM or API key is required; the phenomena are deterministic properties of control flow.

Exposure (C2): A five-model study (GPT-4o, Claude, Gemini, DeepSeek, Llama) measures how often frontier models emit the leak-triggering plan shape under an a-priori protocol. A live end-to-end experiment (Experiment A) drives real models through the unmodified FW-A (LangGraph) runtime and observes \(P(\text{leak} \mid \text{emitted})\). A 13-incident public corpus from three trackers provides a lower-bound occurrence count.

Repair (C3): SOUNDGATE is an environment-external effect gate: every side effect must be admitted through it before touching the world. It enforces four properties mapped to the four violation classes: hold-until-decided (P1), reject-cancels (P2), dedup-on-replay (P3), fence-on-cancel (P4). The admission core is implemented in Rust, exposed over a line-delimited protocol, and bridged to Python via PyO3. Complete mediation—every side-effecting path submits to the gate—is an explicit integration contract, not a silent assumption. Formal verification uses Verus (Rust), TLA+/TLC (to \(7.5 \times 10^7\) states), TLAPS, and Loom; differential conformance testing over \(1.2 \times 10^7\) operations connects the model to the deployed code with zero divergences. Network egress is kernel-enforced by two routes discharging the complete-mediation claim for that channel.

Key Contributions¶

(C1) Model-free measurement characterizing the sibling leak in 5 of 6 frameworks (4 execution models, 2 runtimes), plus replay double-execution, cancellation orphans, and timeout zombies on current releases; cross-framework timeout disagreement mapping the design space; Temporal contrast separating re-architecture gains from residual gaps.
(C2) Exposure study showing frontier models emit the leak-triggering plan shape at rates up to 14%; live end-to-end measurement yielding \(P(\text{leak} \mid \text{emitted}) = 1.00\), \(P(\text{leak}) \leq 0.44\); 13-incident public corpus as an occurrence lower bound.
(C3) SOUNDGATE: a formally verified, framework-independent effect gate with end-to-end repair on all 6 frameworks, 0 fail-closed refusals of legitimate writes on τ-bench retail, and reproducible artifact (all probes, measurement harness, formal models, reference implementation; pip install soundgate).
(C4) Demonstration that prompt-injection-induced leak shapes are blocked by the same gate invariant—intent-agnostic barrier, not injection detection.

Results¶

Sibling leak: Reproduced in all 5 frameworks shipping a pre-execution gate (4 independent designs + 1 cross-language port); FW-E (CrewAI, post-hoc review only) is a design contrast, not a sixth violation.
Live leak rate: 215 of 1,200 end-to-end runs leaked on unmodified FW-A driven by real models; \(P(\text{leak} \mid \text{emitted}) = 1.00\); \(P(\text{leak}) = 0\) once mediated.
Emission rates: Frontier models emit the leak-triggering parallel plan shape at task-dependent, model-disjoint rates up to 14%.
Replay: Double-execution confirmed in both runtimes of the one framework design that re-executes from checkpoint; clean in frameworks caching completed work.
Cancellation/timeout: Thread-backed tools orphan in every framework where constructible; Node pure-async code orphans even on the native AbortSignal surface; four distinct timeout behaviors observed.
SOUNDGATE throughput: ~1 ms per write (gated τ-bench episodes complete with 0 refusals); single-node concurrent load sustains ~12,000 admissions/second (WAL durable mode).
Formal coverage: TLA+/TLC model checked to \(7.5 \times 10^7\) states; \(1.2 \times 10^7\)-operation differential conformance test with zero divergences.

Limitations¶

Complete-mediation contract is a precondition, not a guarantee: if any side-effecting path bypasses the gate (shared filesystem, local IPC, shared memory outside a seccomp/LSM policy), the repair does not apply.
Covers open-source, locally instrumentable runtimes only; hosted/cloud-vendor agent platforms are outside scope.
Formal verification covers a model of the admission core connected to deployed Rust by differential conformance (refinement evidence, not a mechanized refinement proof).
Does not address injection detection, decision authenticity, atomicity across multi-phase APIs, or human-factors concerns (automation bias, vigilance degradation).
Naturalistic τ-bench episodes serialize writes, so the everyday leak gap is latent rather than always triggered; adversarial injection induces it deterministically.
Non-network side-effect channels (filesystem, IPC) require separate policy enforcement; the gate's kernel-enforced route covers network egress only.

Relevance to Harnesses / Meta-Harnesses¶

This paper is directly relevant to harness/meta-harness research because it treats agent frameworks themselves as harnesses—orchestration layers that mediate between LLM outputs and real-world effects—and systematically measures whether their stated control semantics hold. The measurement harness (model-free differential probes, per-framework transcripts, reproducible reproduce.sh) is a meta-harness artifact that audits six production frameworks against a formal contract specification. SOUNDGATE is an external enforcement harness that wraps any inner framework, enforcing effect-admission semantics regardless of the inner runtime's own control flow—exactly the meta-harness pattern of placing a verified enforcement layer outside the component under control. The finding that enforcement gaps recur across independently designed execution models implies that harnesses cannot assume soundness of their inner runtimes and motivates external mediation layers as a general design primitive.