CoChat
Sign Up
PreprintCited by 1Software Testing and Debugging TechniquesDistributed systems and fault toleranceFormal Methods in Verification

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

Open access
Khan, Sajjad·2026·arXiv
DOI 10.48550/arxiv.2607.14166arXiv 2607.14166
Open this paper in CoChat — free account

Abstract

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.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2607.14166

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 66

  1. [1][1] D. J. DeWitt, R. H. Katz, F. Olken, L. D. Shapiro, M. R. Stonebraker, and D. A. Wood, 'Implementation techniques for main memory database systems,' in Proc. ACM SIGMOD , 1984, pp. 1-8. -
  2. [4][4] R. Greenblatt, B. Shlegeris, K. Sachan, and F. Roger, 'AI control: Improving safety despite intentional subversion,' arXiv:2312.06942, 2023. - · arXiv
  3. [7][7] W. M. P. van der Aalst and A. H. M. ter Hofstede, 'YAWL: Yet another workflow language,' Information Systems , vol. 30, no. 4, pp. 245-275, 2005. -
  4. [8][8] R. Pang et al. , 'Zanzibar: Google's consistent, global authorization system,' in Proc. USENIX ATC , 2019, pp. 33-46. -
  5. [11][11] G. Klein et al. , 'seL4: Formal verification of an OS kernel,' in Proc. 22nd ACM SOSP , 2009, pp. 207-220. -
  6. [13][13] P. O. Meredith, D. Jin, D. Griffith, F. Chen, and G. Ros ¸u, 'An overview of the MOP runtime verification framework,' Int. J. Softw. Tools Technol. Transf. , vol. 14, no. 3, pp. 249-289, 2012. -
  7. [14][14] W. M. P. van der Aalst, 'The application of Petri nets to workflow management,' J. Circuits Syst. Comput. , vol. 8, no. 1, pp. 21-66, 1998. -
  8. [15][15] A. D. Birrell and B. J. Nelson, 'Implementing remote procedure calls,' ACM Trans. Comput. Syst. , vol. 2, no. 1, pp. 39-59, 1984. -
  9. [16][16] M. Burrows, 'The Chubby lock service for loosely-coupled distributed systems,' in Proc. 7th USENIX OSDI , 2006, pp. 335-350. -
  10. [19][19] Y. Ruan et al. , 'Identifying the risks of LM agents with an LMemulated sandbox,' in Proc. ICLR , 2024 (arXiv:2309.15817). - · arXiv
  11. [20][20] K. Greshake, S. Abdelnabi, S. Mishra, C. Endres, T. Holz, and M. Fritz, 'Not what you've signed up for: Compromising real-world LLM-integrated applications with indirect prompt injection,' in Proc. 16th ACM Workshop on Artificial Intelligence and Security (AISec) , 2023, pp. 79-90. -
  12. [21][21] R. Parasuraman and V. Riley, 'Humans and automation: Use, misuse, disuse, abuse,' Human Factors , vol. 39, no. 2, pp. 230-253, 1997. -
  13. [23][23] B. Mohammadi, N. Potamitis, L. Klein, A. Arora, and L. Bindschaedler, 'Atomix: Timely, transactional tool use for reliable agentic workflows,' arXiv:2602.14849, 2026. - · arXiv
  14. [24][24] E. Y. Chang and L. Geng, 'SagaLLM: Context management, validation, and transaction guarantees for multi-agent LLM planning,' Proc. VLDB Endow. , vol. 18, no. 12, pp. 4874-4886, 2025. -
  15. [25][25] H. Garcia-Molina and K. Salem, 'Sagas,' in Proc. ACM SIGMOD , 1987, pp. 249-259. -
  16. [26][26] H. Wang, C. M. Poskitt, and J. Sun, 'AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents,' arXiv:2503.18666, 2025. - · arXiv
  17. [27][27] T. Shi, J. He, Z. Wang, H. Li, L. Wu, W. Guo, and D. Song, 'Progent: Programmable privilege control for LLM agents,' arXiv:2504.11703, 2025. - · arXiv
  18. [28][28] E. Debenedetti et al. , 'Defeating prompt injections by design,' arXiv:2503.18813, 2025. - · arXiv
  19. [30][30] P. Helland, 'Idempotence is not a medical condition,' ACM Queue , vol. 10, no. 4, 2012. -
  20. [31][31] D. Lilienthal and S. Hong, 'Mind the gap: Time-of-check to timeof-use vulnerabilities in LLM-enabled agents,' arXiv:2508.17155, 2025. - · arXiv
  21. [32][32] L. Jiang, Z. Liu, H. Luo, and Z. Lin, 'Atomicity for agents: Exposing, exploiting, and mitigating TOCTOU vulnerabilities in browser-use agents,' arXiv:2603.00476, 2026. - · arXiv
  22. [33][33] M. Cemri et al. , 'Why do multi-agent LLM systems fail?' arXiv:2503.13657, 2025. - · arXiv
  23. [34][34] S. Khan, 'Verified detection and prevention of concurrency anomalies in multi-agent large language model systems,' arXiv:2606.17182, 2026. - · arXiv
  24. [35][35] F. B. Schneider, 'Enforceable security policies,' ACM Trans. Inf. Syst. Secur. , vol. 3, no. 1, pp. 30-50, 2000. -
  25. [36][36] M. S. Miller, 'Robust composition: Towards a unified approach to access control and concurrency control,' Ph.D. dissertation, Johns Hopkins University, 2006. -
  26. [37][37] M. Kleppmann, Designing Data-Intensive Applications . O'Reilly, 2017, ch. 8-9 (fencing tokens and generation numbers). -
  27. [38][38] J. Gray and A. Reuter, Transaction Processing: Concepts and Techniques . Morgan Kaufmann, 1993. -
  28. [39][39] L. Orseau and S. Armstrong, 'Safely interruptible agents,' in Proc. 32nd Conf. Uncertainty in Artificial Intelligence (UAI) , 2016, pp. 557566. -
  29. [40][40] N. Soares, B. Fallenstein, S. Armstrong, and E. Yudkowsky, 'Corrigibility,' in AAAI Workshop on AI and Ethics , 2015. -
  30. [43][43] E. G. Young, P. Zhu, T. Caraza-Harter, A. C. Arpaci-Dusseau, and R. H. Arpaci-Dusseau, 'The true cost of containing: A gVisor case study,' in Proc. 11th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud) , 2019. -
  31. [45][45] J. Armstrong, 'Making reliable distributed systems in the presence of software errors,' Ph.D. dissertation, KTH Royal Institute of Technology, Stockholm, 2003. -
  32. [47][47] J. Ligatti, L. Bauer, and D. Walker, 'Edit automata: Enforcement mechanisms for run-time security policies,' Int. J. Inf. Secur. , vol. 4, no. 1-2, pp. 2-16, 2005. -
  33. [48][48] A. Birgisson, J. G. Politz, ´ U. Erlingsson, A. Taly, M. Vrable, and M. Lentczner, 'Macaroons: Cookies with contextual caveats for decentralized authorization in the cloud,' in Proc. Network and Distributed System Security Symposium (NDSS) , 2014. -
  34. [49][49] R. N. M. Watson, J. Anderson, B. Laurie, and K. Kennaway, 'Capsicum: Practical capabilities for UNIX,' in Proc. 19th USENIX Security Symposium , 2010. -
  35. [50][50] R. N. M. Watson et al. , 'CHERI: A hybrid capability-system architecture for scalable software compartmentalization,' in Proc. IEEE Symposium on Security and Privacy , 2015. -
  36. [52][52] W. M. McKeeman, 'Differential testing for software,' Digital Technical Journal , vol. 10, no. 1, pp. 100-107, 1998. -
  37. [53][53] X. Yang, Y. Chen, E. Eide, and J. Regehr, 'Finding and understanding bugs in C compilers,' in Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI) , 2011. -
  38. [54][54] D. Ongaro and J. Ousterhout, 'In search of an understandable consensus algorithm,' in Proc. USENIX Annual Technical Conference (ATC) , 2014. -
  39. [55][55] L. A. Dennis, M. Fisher, M. P. Webster, and R. H. Bordini, 'Model checking agent programming languages,' Automated Software Engineering , vol. 19, no. 1, 2012. -
  40. [56][56] X. Liu et al. , 'AgentBench: Evaluating LLMs as agents,' in Proc. Int. Conf. Learning Representations (ICLR) , 2024. -
  41. [57][57] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, 'IronFleet: Proving practical distributed systems correct,' in Proc. ACM Symp. Operating Systems Principles (SOSP) , 2015. -
  42. [58][58] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson, 'Verdi: A framework for implementing and formally verifying distributed systems,' in Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI) , 2015. -
  43. [59][59] H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich, 'Using Crash Hoare Logic for certifying the FSCQ file system,' in Proc. ACM Symp. Operating Systems Principles (SOSP) , 2015. -
  44. [62][62] International Electrotechnical Commission, 'IEC 61508: Functional safety of electrical/electronic/programmable electronic safetyrelated systems,' Edition 2.0, IEC, Geneva, 2010. -
  45. [65][65] K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger, 'The notions of consistency and predicate locks in a database system,' Commun. ACM , vol. 19, no. 11, pp. 624-633, 1976. -
  46. [66][66] F. Momot, S. Bratus, S. M. Hallberg, and M. L. Patterson, 'The seven turrets of Babel: A taxonomy of LangSec errors and how to expunge them,' in Proc. IEEE Cybersecurity Development (SecDev) , 2016, pp. 45-52. -
  47. [68][68] S. Yao, N. Shinn, P. Razavi, and K. Narasimhan, ' τ -bench: A benchmark for tool-agent-user interaction in real-world domains,' arXiv:2406.12045, 2024. - · arXiv
  48. [69][69] R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, 'Efficient software-based fault isolation,' in Proc. 14th ACM Symp. Operating Systems Principles (SOSP) , 1993, pp. 203-216. -
  49. [70][70] J. M. Lucassen and D. K. Gifford, 'Polymorphic effect systems,' in Proc. 15th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL) , 1988, pp. 47-57. -
  50. [71][71] M. Leucker and C. Schallhart, 'A brief account of runtime verification,' J. Logic and Algebraic Programming , vol. 78, no. 5, pp. 293-303, 2009. -
  51. [72][72] T. Akidau, A. Balikov, K. Bekiro˘ glu, S. Chernyak, J. Haberman, R. Lax, S. McVeety, D. Mills, P. Nordstrom, and S. Whittle, 'MillWheel: Fault-tolerant stream processing at Internet scale,' Proc. VLDB Endowment , vol. 6, no. 11, pp. 1033-1044, 2013. -
  52. [73][73] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, 'How Amazon Web Services uses formal methods,' Commun. ACM , vol. 58, no. 4, pp. 66-73, 2015. -
  53. [75][75] W. M. P. van der Aalst, A. H. M. ter Hofstede, B. Kiepuszewski, and A. P. Barros, 'Workflow patterns,' Distributed and Parallel Databases , vol. 14, no. 1, pp. 5-51, 2003. -
  54. [76][76] M. C. Loring, M. Marron, and D. Leijen, 'Semantics of asynchronous JavaScript,' in Proc. 13th ACM SIGPLAN Int. Symp. Dynamic Languages (DLS) , 2017, pp. 51-62. -
  55. [77][77] P. Carbone, S. Ewen, G. F´ ora, S. Haridi, S. Richter, and K. Tzoumas, 'State management in Apache Flink: Consistent stateful distributed stream processing,' Proc. VLDB Endowment , vol. 10, no. 12, pp. 17181729, 2017. -
  56. [78][78] C. Packer, S. Wooders, K. Lin, V. Fang, S. G. Patil, I. Stoica, and J. E. Gonzalez, 'MemGPT: Towards LLMs as operating systems,' arXiv:2310.08560, 2023. - · arXiv
  57. [79][79] K. Mei, Z. Li, S. Xu, R. Ye, Y. Ge, and Y. Zhang, 'AIOS: LLM agent operating system,' arXiv:2403.16971, 2024. - · arXiv
  58. [80][80] R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer, 'RustBelt: Securing the foundations of the Rust programming language,' Proc. ACM Program. Lang. , vol. 2, no. POPL, pp. 66:1-66:34, 2018. -
  59. [81][81] L. Bainbridge, 'Ironies of automation,' Automatica , vol. 19, no. 6, pp. 775-779, 1983. -
  60. [84][84] J. Gray, 'Notes on data base operating systems,' in Operating Systems: An Advanced Course , ser. Lecture Notes in Computer Science, vol. 60. Springer, 1978, pp. 393-481. -
  61. [85][85] A. Thomson, T. Diamond, S.-C. Weng, K. Ren, P. Shao, and D. J. Abadi, 'Calvin: Fast distributed transactions for partitioned database systems,' in Proc. ACM SIGMOD , 2012, pp. 1-12. -
  62. [86][86] M. R. Endsley, 'Toward a theory of situation awareness in dynamic systems,' Human Factors , vol. 37, no. 1, pp. 32-64, 1995. -
  63. [87][87] M. L. Cummings, 'Automation bias in intelligent time critical decision support systems,' in Proc. AIAA 1st Intelligent Systems Technical Conference , 2004. -
  64. [89][89] E. Debenedetti, J. Zhang, M. Balunovi´ c, L. Beurer-Kellner, M. Fischer, and F. Tram` er, 'AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents,' in Proc. NeurIPS Datasets and Benchmarks , 2024 (arXiv:2406.13352). - · arXiv
  65. [90][90] Y. Wu, F. Roesner, T. Kohno, N. Zhang, and U. Iqbal, 'IsolateGPT: An execution isolation architecture for LLM-based agentic systems,' in Proc. Network and Distributed System Security Symposium (NDSS) , 2025 (arXiv:2403.04960). - · arXiv
  66. [91][91] ´ U. Erlingsson and F. B. Schneider, 'IRM enforcement of Java stack inspection,' in Proc. IEEE Symp. Security and Privacy , 2000, pp. 246-255. -

Cited by

Sorted by citations

Authors
Khan, S.
Corresponding author
Khan, Sajjad
ORCID
Khan, Sajjad
Venue
arXiv
Publisher
arXiv
Published
2026
Pages
1-1
ISSN
2169-3536 (ISSN-L)
DOI
10.48550/arxiv.2607.14166
arXiv
2607.14166
OpenAlex
W7169508870
Cited by
0
References
0
FWCI
0.00
Type
journal article
Language
en
Open access
Licence
Locations
  • IEEE Access (publishedVersion, cc-by)
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
Topics
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Computer Networks and Communications › Distributed systems and fault tolerance
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
LLM agents, agent frameworks, control primitives, enforcement gaps, formal verification

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review