FlagThis

Abstract

Production LLM-agent frameworks expose _control primitives_ human-in-the-loop approval gates, run cancellation, and execution timeoutswhose names, documentation, and practitioner guidance imply _barrier_ semantics: while a run is paused, cancelled, or timed out, no gated side effect executes. We show this implied contract holds on none of the six widely used open-source frameworks we evaluate. Model-free differential probes isolate a recurring _sibling leak_ an approval gate suspends its own branch while a sibling branchs effect executes _during the pause_ , so a subsequent rejection cannot prevent itin every evaluated framework that ships a pre-execution gate (five of six, spanning four execution models and two language runtimes; the sixth ships post-hoc review only), and confirm three further gaps on current releases: replay double-execution, cancellation orphans, and timeout zombies. The hazard is reachable, not merely constructible. Under a protocol fixed a priori, frontier models emit the leak-triggering plan shape at pooled rates up to 14%sharply task-dependent and model-disjoint, every near-zero rate re-measured on a second serving pathand when live models drive the unmodified frameworks under an approval pause, 215 of 1 _,_ 200 unmediated runs execute their effect during the pause, _P_ (leak _|_ emitted)=1 _._ 00 in every emitting arm, across three schedulers and two language runtimes. We are equally explicit about where the shape does _not_ arise: on naturalistic __ -bench episodes models serialize their writes, so the everyday gap is _latent_ rather than prevalent; under adversarial injection it is induced deterministically, and a verified 13-incident public corpus corroborates the replay and cancellation failures third-party. To repair the measured gaps we present SOUNDGATE, a small _environment-external_ effect gatea language-independent arbiter in Rust through which every side effect must be admittedenforcing hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel, one property per measured violation class, under an explicitly stated _complete-mediation_ contract: the classical reference-monitor assumption, discharged for network egress by two implemented, kernel-enforced routes (a loopback-only namespace; cgroup eBPF hooks) under which an unwrapped tools external action fails closed rather than silently leaking. We mechanically verify the properties over a _model_ of the admission core (Verus; TLA+/TLC, exhaustive to 7 _._ 5 __ 10[7] states; TLAPS induction), model-check the deployed concurrent Rust with Loom, and bridge model to code by differential conformance over 1 _._ 2 __ 10[7] operations with zero divergencesrefinement _evidence_ , not a mechanized refinement proof; the effort surfaced two real defects. Under the stated contract, SOUNDGATE blocks every measured violation in end-to-end replay on all six frameworks while releasing legitimate approved effects: gated __ -bench episodes complete with zero fail-closed refusals at __ 1 ms admission per write, and group-committed durable admission sustains __ 12k26k admissions per second.