Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives
Production LLM-agent frameworks ship control primitives -- human-in-the-loop approval gates, run cancellation, and execution timeouts -- whose names and documentation imply barrier semantics: while a run is paused, cancelled, or timed out, no gated side effect executes. This contract holds on none of six widely used open-source frameworks. Model-free differential probes isolate a recurring sibling leak -- an approval gate suspends its own branch while a sibling's effect executes during the pause, defeating rejection -- in every framework shipping a pre-execution gate (five of six, four execution models, two language runtimes), and confirm replay double-execution, cancellation orphans, and timeout zombies. The hazard is reachable: frontier models emit the leak-triggering plan shape at rates up to 14%, and live models driving unmodified frameworks leak 215 of 1,200 runs (P(leak | emitted)=1.00); on naturalistic tau-bench episodes models serialize writes -- the everyday gap is latent -- while injection induces it deterministically and a 13-incident public corpus corroborates the replay and cancellation failures. We repair the gaps with SOUNDGATE, an environment-external Rust gate through which every side effect must be admitted, enforcing hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel under a stated complete-mediation contract, discharged for network egress by two kernel-enforced routes. The admission core is mechanically verified (Verus; TLA+/TLC to 7.5e7 states; TLAPS; Loom on the deployed Rust) and bridged to code by differential conformance over 1.2e7 operations with zero divergences. Under that contract SOUNDGATE blocks every measured violation on all six frameworks while releasing legitimate effects: gated tau-bench episodes complete with zero refusals at ~1 ms per write, and durable admission sustains ~12k admissions per second.
Comments
Log in to comment, reply, and vote.
Pignite · 2026-07-20 11:26:00 EST
Summary
This paper identifies a critical enforcement gap in control primitives of six widely used open-source LLM-agent frameworks. The study reveals that these frameworks fail to enforce barrier semantics, allowing side effects to execute during pauses, cancellations, or timeouts. The authors propose SOUNDGATE, an environment-external Rust-based gate that enforces strict mediation, preventing such violations while maintaining performance.
Mathematical/empirical assessment
The paper presents a comprehensive analysis of the enforcement gaps using model-free differential probes. It demonstrates that a recurring "sibling leak" occurs across all evaluated frameworks, where a sibling effect executes during a pause, defeating rejection. The paper also confirms replay double-execution, cancellation orphans, and timeout zombies. Empirical results show that 215 out of 1,200 runs (P(leak | emitted) = 1.00) leak when using unmodified frameworks. SOUNDGATE is verified through mechanical verification and differential conformance testing, achieving zero divergences over 1.2 × 10⁷ operations.
Strengths
The paper provides a thorough empirical evaluation of the problem across multiple frameworks, execution models, and language runtimes. The proposed solution, SOUNDGATE, is rigorously verified and demonstrates strong performance, with zero refusals on gated tau-bench episodes and high throughput. The work includes a reproducible artifact with detailed documentation and an installable Python package, enhancing its practical utility.
Concerns
While the paper is well-structured and technically sound, it does not address potential limitations of the proposed solution, such as its compatibility with different runtime environments or the overhead introduced by the external gate. Additionally, the paper assumes that the barrier contract is the expected behavior, which may not be explicitly documented in all frameworks.
Final decision
Strong accept