Pith. sign in

REVIEW 2 major objections 4 minor 94 references

The paper claims that the stop primitives in agent frameworks—approval gates, cancellation, and timeouts—fail to provide barrier semantics, and that a 'sibling leak' lets side effects execute during approval pauses; it then repairs the gap

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 05:06 UTC pith:VPGBWAHR

load-bearing objection A careful, artifact-heavy measurement showing that approval/cancel/timeout primitives in six agent frameworks do not provide barrier semantics, plus a verified external repair; the main caveat is that 'executes' is measured at a single in-process commit point. the 2 major comments →

arxiv 2607.14166 v2 pith:VPGBWAHR submitted 2026-07-15 cs.SE cs.CRcs.DC

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

Sajjad Khan This is my paper
classification cs.SE cs.CRcs.DC
keywords agent frameworkscontrol primitiveshuman-in-the-loopapproval gatessibling leakbarrier semanticscancellationSOUNDGATE
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to establish that the control primitives agent frameworks ship as safety mechanisms—human-approval gates, run cancellation, and execution timeouts—do not provide the barrier semantics their names imply. Its central measured claim is the 'sibling leak': when a side-effecting action runs alongside an approval gate in the same execution step, the gate suspends only its own branch while the sibling's effect commits during the pause, so a later human rejection cannot prevent it. The leak reproduces in every evaluated framework that ships a pre-execution gate, spanning four execution models and two language runtimes, and live models driving unmodified frameworks leaked 215 of 1,200 runs. The paper also presents SOUNDGATE, an environment-external gate that holds effects until a decision and blocks every measured violation class under a stated complete-mediation contract. A sympathetic reader would care because the work turns a trusted safety assumption into a measured, repairable gap rather than a matter of faith.

Core claim

The paper's central discovery is the sibling leak: an approval interrupt suspends only the branch that raises it, while a sibling branch in the same step commits its effect before control returns to any caller that could deliver a decision. The paper defines a barrier contract—no gated effect between pause and decision, no rejected effect ever executing, no effect more than once, and nothing landing after cancellation or timeout—and shows by model-free differential probes that none of six widely used open-source frameworks satisfies it. Sibling leak and reject-after-effect appear in every framework that ships a pre-execution gate; replay double-execution, cancellation orphans, and timeout zo

What carries the argument

The central object is the sibling leak itself, understood as a schedulability property: the pause halts the scheduling loop only after the pausing superstep, so any effect concurrent with the gate in that step commits. The repair is SOUNDGATE, an environment-external Rust gate acting as the single admission point through which every side effect must pass before externalizing. It keys effects by (run, identity) and enforces four properties—hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel—so no effect is released without a verdict, regardless of how the framework's own scheduler races.

Load-bearing premise

The whole result rests on the assumption that every side effect has a single interceptable commit point and that every side-effecting path really does submit to the gate (complete mediation); if effects externalize in multiple phases, through filesystem/IPC/shared memory, or via an unwrapped tool, the measured verdict and the repair do not transfer.

What would settle it

Run the minimal sibling-leak probe—an approval gate and a side-effecting sibling in the same execution step—on any framework that ships a pre-execution gate, with no gate interposed. The paper predicts the sibling commits during the pause in every case (P(leak|emitted)=1.00 end-to-end); one emitted shape that does not leak, or one clean run in its randomized sweep (predicted 577/577), would falsify the universality claim.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • A deployment that gates an irreversible action behind an approval pause has been relying on a false guarantee: an emitted sibling effect lands before any human decision can stop it.
  • The recurrence across four execution models and two language runtimes means the gap is a property of the concurrent-pause pattern, not a single implementation bug.
  • SOUNDGATE restores the barrier for mediated effects, blocking every measured violation class on all six frameworks while releasing legitimate effects at roughly one millisecond per write.
  • Moving to a durable-execution engine closes only the replay axis by construction; the approval-pause barrier still requires an admission point outside the workflow.
  • Naturalistic model behavior mostly serializes writes, so the gap is latent today, but adversarial input or parallel tool-calling defaults would activate it.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A natural next step is a barrier-semantics conformance suite: turn the four contract clauses into regression predicates that framework releases must pass before shipping.
  • The single-commit-point model suggests the measured gap likely understates real-world exposure, since multi-phase APIs need per-phase admission and non-network channels remain outside the structural enforcement routes.
  • If parallel tool-calling becomes the default in agent runtimes, the latent gap may widen faster than the paper's naturalistic baseline suggests, increasing the value of an external admission point.
  • The same admission pattern extends to other irreversible actuations only where a discrete commit point exists for a wrapper to intercept; effects that externalize through shared filesystems, IPC, or shared memory require a wider mediation envelope than the one demonstrated.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper claims that the barrier semantics implied by agent-framework control primitives—approval gates, cancellation, timeouts, i.e., 'stop means stop'—hold on none of six evaluated open-source frameworks. Model-free deterministic probes with pre-registered violation predicates (B1–B4) isolate a 'sibling leak': when an approval gate and a side-effecting action are siblings in one execution step, the gate suspends its own branch while the sibling's effect commits during the pause, so a human rejection cannot prevent it. This is reproduced in every gate-shipping framework (five of six; four execution models; two language runtimes) and localized by a 1,000-graph randomized structural sweep. The paper also confirms replay double-execution, cancellation orphans, and timeout zombies. Exposure studies show frontier models emit the leak-triggering plan shape at task-dependent rates, and live end-to-end runs leak 215/1,200 effects unmediated (P(leak|emitted)=1.00 on every emitting arm) versus 0/1,200 mediated. The proposed repair, SOUNDGATE, is an environment-external Rust gate enforcing hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel under a stated complete-mediation contract, with mechanical verification (Verus, TLA+/TLC, TLAPS, Loom) bridged to the deployed code by differential conformance; it blocks all measured violations on all six frameworks at ~1 ms per write with no fail-closed refusals of legitimate effects.

Significance. The measurement, if correct, is a significant and timely result: it converts scattered practitioner suspicion into a characterized, cross-framework enforcement gap using deterministic, model-free probes with pre-registered predicates, a 1,000-graph randomized sweep (577/577 concurrent effects leak, 0/363 descendants), and reproduction across four execution models, two runtimes, and multiple environments. The live end-to-end arms turn the proxy into an executed outcome (215/1,200 leaks unmediated versus 0/1,200 mediated) and the Temporal contrast cleanly separates what re-architecture buys from what it does not. The repair is unusually well-scoped: SOUNDGATE's claims are conditional on a stated complete-mediation contract, discharged by wrapper discipline, a static linter, and two kernel-enforced structural routes; the admission core is mechanically verified and bridged to the deployed Rust by differential conformance over 1.2×10^7 operations with zero divergences, with an executable artifact and single-command audit. The explicit limitation statements on phase-grained mediation, non-network channels, and the latent everyday gap strengthen rather than weaken credibility.

major comments (2)
  1. [Abstract / §2, 'What executes means'] The headline claim 'this contract holds on none of six widely used open-source frameworks' is stated in operator terms, but B1–B4 are measured at a single commit point instrumented by an in-process event-log append (§3.1). For effects whose externalization is not co-located with the tool call—multi-phase authorize-then-capture APIs, asynchronous enqueue/callback flows, or non-network channels such as a shared filesystem/IPC—neither the universal statement nor P(leak|emitted)=1.00 (§4.2) is demonstrated. Section 6.4 acknowledges and scopes this ('phase-grained mediation'; non-network residue), so I am not asking for new experiments; but the abstract and C1 (§1) should carry the qualifier that the measured claim covers effects modeled at a single commit point, so the headline cannot be read as universal over all externalization modes.
  2. [§4.1–4.2, Table 4] The 'up to 14%' pooled exposure and the 215/1,200 end-to-end leak count come from ten authored tasks deliberately engineered to create the leak condition; the naturalistic τ-bench baseline (§6.4) shows 0/71 gated batches co-emitting a benign read, with models serializing writes. The body is scrupulous about this, but the abstract's juxtaposition of 'hazard is reachable—rates up to 14%—live models leak 215 of 1,200' will read to many as a naturalistic incidence claim. Please add one sentence in the abstract (and where C2 is introduced) tying these figures to the controlled-task protocol and to the explicitly latent everyday gap.
minor comments (4)
  1. [Abstract] The parenthetical 'P(leak|emitted)=1.00 (215/1,200 leaks unmediated [...] 0/1,200 mediated)' aggregates four arms, two of which emitted nothing (deepseek-chat: 0/300). The conditional is per emitting arm (133/133, 26/26, 56/56). Suggest: 'P(leak|emitted)=1.00 on every emitting arm (215/1,200 overall unmediated; 0/1,200 mediated).'
  2. [Table 4 / §4.1] The abstract's 'rates up to 14%' refers to GPT-4o's pooled exposure; Llama's provider-direct replication reaches 0.90 on compound_cleanup (conditional on called runs). State once in §4.1 which rate the headline sentence refers to, to avoid the impression that 14% is the maximum over all cells.
  3. [§5.2, Figure 2] Figure 2 shows only the SUBMIT function; the DECIDE and CANCEL behavior is carried in the caption. Consider including a few lines of pseudocode for DECIDE (including the fence path when the run is cancelled) in the figure, since the admission-priority statement in the text is the kind of detail a reader will want adjacent to Algorithm 2.
  4. [Table 2, 'Cancel: pure async' row] The row has '–' cells for FW-B and FW-E, but the §3.3 interpretation states that 'cancellation is clean when the tool is a pure-async coroutine under Python's asyncio.' Please clarify whether that clean result is FW-A only, and whether '–' for FW-B/E means the configuration was not probed or is not expressible; the per-cell distinction is in the artifact but should be readable from the caption.

Circularity Check

0 steps flagged

No significant circularity: the leak measurement is independent of the repair, the P1–P4/B1–B4 mapping is explicitly disclosed and discharged non-vacuously, and the only self-citation ([34]) is non-load-bearing.

full rationale

The paper's central claim (C1) is an empirical measurement of framework scheduler behavior, and it is self-contained and externally falsifiable: probes are model-free and deterministic, verdicts reproduce across >=3 environments and two releases of FW-A, and the barrier contract B1-B4 is grounded in vendor wording ('pause graph execution at specific points' [22]) and a maintainer-filed issue, not derived from the measurement. The randomized structural sweep (577/577 concurrent-same-superstep leaks vs 0/331 later-superstep, 0/363 descendants) shows the leak is a scheduler property, not an artifact of probe construction. Section 4.2 explicitly disclaims predictive content for P(leak|emitted)=1.00, calling it a confirmation of Section 3's mechanism and locating the genuinely contingent quantity in P(emitted). The one reduction-shaped loop is the explicit correspondence in Definition 1 ('B1-B4 are exactly the violation predicates of Section 3 and the enforcement properties P1-P4 of Section 5'), but the paper itself raises and answers the reference-monitor tautology objection: the verification tiers are machine-checked (Verus, TLA+/TLC, TLAPS, Loom) and surfaced two real implementation defects (cross-run key-reuse clobber; compaction ordering bug), so 'a gate enforcing P1-P4 enforces P1-P4' is non-vacuous, and the end-to-end 'closes' claims are executed against real frameworks under an explicitly stated complete-mediation contract. The only self-citation is [34] (the author's own prior arXiv work), used as related-work territory in Section 6.4 and Related Work, not as load-bearing evidence for any claim. Acknowledged scope limits (single commit-point model; non-network channels under the placement contract) are limitations, not circularity: the single real HTTP-POST demonstration and the tau-bench/episode completions anchor the metric externally. Verdict: the measurement stands independently; the repair is conditional by explicit design; no step reduces to its inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

No quantity is fitted to data. All test sizes (N=100 per task, 300 runs per experiment arm), pause values, and verification domain sizes (2x2, 3x3, 4x3) are stated a priori as protocol choices or verification scale parameters; the WAL group-commit cap (512) and TTL (0.5 s) are design constants. The paper's 'leak rate' statistics are empirical estimates with Wilson intervals, not fitted values. SOUNDGATE is a concrete engineered artifact (state machine plus socket protocol) with shipped code and tests; it is not a postulated entity with unobserved consequences. No new physical or mathematical entities are introduced; the (run, key) admission identity is a design construct that any reader can falsifiably test against the artifact.

axioms (5)
  • domain assumption Each side effect has a single well-defined commit point, and in-process event-log appends faithfully mark that point.
    Used to define 'executes' (Section 2, 'What executes means') and to instrument every probe (Section 3.1: each tool's single effect-log append sits exactly there). Multi-phase APIs and non-network channels are excluded; the paper scopes this in Section 6.4.
  • domain assumption The barrier contract B1-B4 is implied by framework names and documentation and is the operator expectation.
    Section 2.1 grounds B1-B4 in vendor wording and a maintainer-filed issue; if maintainers disclaim barrier semantics, the 'contract mismatch' headline weakens. The paper acknowledges it is an implied, not formal, contract.
  • domain assumption The six selected frameworks instantiate the dominant execution-model families, so recurrence indicates a general gap.
    Section 3.1 inclusion criteria (Pregel/BSP, event bus, message-passing fan-out, parallel tool calls) and Section 6.5 external validity. Hosted/closed platforms are unprobed.
  • domain assumption The TLA+/TLAPS/Verus model faithfully abstracts the deployed Rust admission core.
    Section 5.5: verification covers 'a model of the admission core'; the bridge to deployed code is differential conformance (1.2e7 ops, zero divergence), bounded-exhaustive checks, and Loom, not a mechanized refinement proof. The paper says this explicitly.
  • domain assumption Kernel-level mediation routes (netns, cgroup eBPF, seccomp/Landlock) enforce as documented and are Linux-only.
    Section 5, 'Making mediation structural' and Table 6; non-network channels and non-Linux OSes remain under the placement contract (Section 6.4).

pith-pipeline@v1.3.0-alltime-deepseek · 49907 in / 21417 out tokens · 196655 ms · 2026-08-02T05:06:40.030694+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2607.14166 by Sajjad Khan.

Figure 1
Figure 1. Figure 1: The sibling leak and its repair. Top: an approval pause suspends [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: SOUNDGATE admission. DECIDE(run, key, approved) removes the pending effect under that identity and releases it only if approved and its run is not cancelled; deciding a cancelled run’s effect reports REFUSEDCANCELLED (the fence, not a “duplicate”, is the reason). CANCEL(run) marks the run and drops its held effects. Property 2 (Reject-cancels). A rejected effect is never released and remains refused on res… view at source ↗
Figure 3
Figure 3. Figure 3: What is proved, and how it connects to what runs. The three [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

94 extracted references · 14 linked inside Pith

  1. [1]

    Implementation techniques for main memory database systems,

    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,” inProc. ACM SIGMOD, 1984, pp. 1–8

    1984

  2. [2]

    Event sourcing,

    M. Fowler, “Event sourcing,” https://martinfowler.com/eaaDev/ EventSourcing.html, 2005, accessed July 2026

    2005

  3. [3]

    External authorization ( ext_authz) filter,

    Envoy Project Authors, “External authorization ( ext_authz) filter,” Envoy proxy documentation, https://www.envoyproxy. io/docs/envoy/latest/intro/arch overview/security/ext authz filter, accessed July 2026

    2026

  4. [4]

    AI control: Improving safety despite intentional subversion,

    R. Greenblatt, B. Shlegeris, K. Sachan, and F. Roger, “AI control: Improving safety despite intentional subversion,” arXiv:2312.06942, 2023

    Pith/arXiv arXiv 2023

  5. [5]

    tokio::select!: cancellation safety,

    Tokio contributors, “tokio::select!: cancellation safety,” Tokio API documentation, https://docs.rs/tokio/latest/tokio/macro. select.html, accessed July 2026

    2026

  6. [6]

    Loom: concurrency permutation testing for Rust,

    Tokio contributors, “Loom: concurrency permutation testing for Rust,” https://docs.rs/loom, accessed July 2026

    2026

  7. [7]

    YAWL: Yet another workflow language,

    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

    2005

  8. [8]

    Zanzibar: Google’s consistent, global authorization system,

    R. Panget al., “Zanzibar: Google’s consistent, global authorization system,” inProc. USENIX ATC, 2019, pp. 33–46

    2019

  9. [9]

    Model Context Protocol,

    Anthropic, “Model Context Protocol,” specification, https:// modelcontextprotocol.io, 2024, accessed July 2026

    2024

  10. [10]

    Microsoft Agent Framework overview,

    Microsoft, “Microsoft Agent Framework overview,” https:// learn.microsoft.com/en-us/agent-framework/overview/, 2026, ac- cessed July 2026

    2026

  11. [11]

    seL4: Formal verification of an OS kernel,

    G. Kleinet al., “seL4: Formal verification of an OS kernel,” inProc. 22nd ACM SOSP, 2009, pp. 207–220

    2009

  12. [12]

    Computer security technology planning study,

    J. P . Anderson, “Computer security technology planning study,” U.S. Air Force Electronic Systems Division, Tech. Rep. ESD-TR-73- 51, 1972

    1972

  13. [13]

    An overview of the MOP runtime verification framework,

    P . O. Meredith, D. Jin, D. Griffith, F. Chen, and G. Ro s ¸u, “An overview of the MOP runtime verification framework,”Int. J. Softw. Tools Technol. Transf., vol. 14, no. 3, pp. 249–289, 2012

    2012

  14. [14]

    The application of Petri nets to workflow management,

    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

    1998

  15. [15]

    Implementing remote procedure calls,

    A. D. Birrell and B. J. Nelson, “Implementing remote procedure calls,”ACM Trans. Comput. Syst., vol. 2, no. 1, pp. 39–59, 1984

    1984

  16. [16]

    The Chubby lock service for loosely-coupled dis- tributed systems,

    M. Burrows, “The Chubby lock service for loosely-coupled dis- tributed systems,” inProc. 7th USENIX OSDI, 2006, pp. 335–350

    2006

  17. [17]

    Idempotent requests,

    Stripe, “Idempotent requests,” API documentation, https://docs. stripe.com/api/idempotent requests, accessed July 2026

    2026

  18. [18]

    Admission control in Kuber- netes,

    The Kubernetes Authors, “Admission control in Kuber- netes,” https://kubernetes.io/docs/reference/access-authn- authz/admission-controllers/, accessed July 2026

    2026

  19. [19]

    Identifying the risks of LM agents with an LM- emulated sandbox,

    Y. Ruanet al., “Identifying the risks of LM agents with an LM- emulated sandbox,” inProc. ICLR, 2024 (arXiv:2309.15817)

    Pith/arXiv arXiv 2024

  20. [20]

    Not what you’ve signed up for: Compromising real-world LLM-integrated applications with indirect prompt injection,

    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

    2023

  21. [21]

    Humans and automation: Use, misuse, disuse, abuse,

    R. Parasuraman and V . Riley, “Humans and automation: Use, misuse, disuse, abuse,”Human Factors, vol. 39, no. 2, pp. 230–253, 1997

    1997

  22. [22]

    LangGraph documentation: Graph API and interrupts,

    LangChain, “LangGraph documentation: Graph API and interrupts,” https://docs.langchain.com/oss/python/langgraph/ graph-api and https://docs.langchain.com/oss/python/ langgraph/interrupts, accessed July 2026

    2026

  23. [23]

    Atomix: Timely, transactional tool use for reliable agentic workflows,

    B. Mohammadi, N. Potamitis, L. Klein, A. Arora, and L. Bind- schaedler, “Atomix: Timely, transactional tool use for reliable agentic workflows,” arXiv:2602.14849, 2026

    Pith/arXiv arXiv 2026

  24. [24]

    SagaLLM: Context management, vali- dation, and transaction guarantees for multi-agent LLM planning,

    E. Y. Chang and L. Geng, “SagaLLM: Context management, vali- dation, and transaction guarantees for multi-agent LLM planning,” Proc. VLDB Endow., vol. 18, no. 12, pp. 4874–4886, 2025

    2025

  25. [25]

    Garcia-Molina and K

    H. Garcia-Molina and K. Salem, “Sagas,” inProc. ACM SIGMOD, 1987, pp. 249–259

    1987

  26. [26]

    AgentSpec: Customiz- able runtime enforcement for safe and reliable LLM agents,

    H. Wang, C. M. Poskitt, and J. Sun, “AgentSpec: Customiz- able runtime enforcement for safe and reliable LLM agents,” arXiv:2503.18666, 2025

    Pith/arXiv arXiv 2025

  27. [27]

    Progent: Programmable privilege control for LLM agents,

    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

    Pith/arXiv arXiv 2025

  28. [28]

    Defeating prompt injections by design,

    E. Debenedettiet al., “Defeating prompt injections by design,” arXiv:2503.18813, 2025

    Pith/arXiv arXiv 2025

  29. [29]

    Temporal: Durable execution platform,

    Temporal Technologies, “Temporal: Durable execution platform,” https://temporal.io, accessed July 2026

    2026

  30. [30]

    Idempotence is not a medical condition,

    P . Helland, “Idempotence is not a medical condition,”ACM Queue, vol. 10, no. 4, 2012

    2012

  31. [31]

    Mind the gap: Time-of-check to time- of-use vulnerabilities in LLM-enabled agents,

    D. Lilienthal and S. Hong, “Mind the gap: Time-of-check to time- of-use vulnerabilities in LLM-enabled agents,” arXiv:2508.17155, 2025

    Pith/arXiv arXiv 2025

  32. [32]

    Atomicity for agents: Exposing, exploiting, and mitigating TOCTOU vulnerabilities in browser-use agents,

    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 2026

  33. [33]

    Why do multi-agent LLM systems fail?

    M. Cemriet al., “Why do multi-agent LLM systems fail?” arXiv:2503.13657, 2025

    Pith/arXiv arXiv 2025

  34. [34]

    Verified detection and prevention of concurrency anomalies in multi-agent large language model systems,

    S. Khan, “Verified detection and prevention of concurrency anomalies in multi-agent large language model systems,” arXiv:2606.17182, 2026

    Pith/arXiv arXiv 2026

  35. [35]

    Enforceable security policies,

    F. B. Schneider, “Enforceable security policies,”ACM Trans. Inf. Syst. Secur., vol. 3, no. 1, pp. 30–50, 2000

    2000

  36. [36]

    Robust composition: Towards a unified approach to access control and concurrency control,

    M. S. Miller, “Robust composition: Towards a unified approach to access control and concurrency control,” Ph.D. dissertation, Johns Hopkins University, 2006

    2006

  37. [37]

    Kleppmann,Designing Data-Intensive Applications

    M. Kleppmann,Designing Data-Intensive Applications. O’Reilly, 2017, ch. 8–9 (fencing tokens and generation numbers)

    2017

  38. [38]

    Gray and A

    J. Gray and A. Reuter,Transaction Processing: Concepts and Techniques. Morgan Kaufmann, 1993

    1993

  39. [39]

    Safely interruptible agents,

    L. Orseau and S. Armstrong, “Safely interruptible agents,” inProc. 32nd Conf. Uncertainty in Artificial Intelligence (UAI), 2016, pp. 557– 566. 31

    2016

  40. [40]

    Corri- gibility,

    N. Soares, B. Fallenstein, S. Armstrong, and E. Yudkowsky, “Corri- gibility,” inAAAI Workshop on AI and Ethics, 2015

    2015

  41. [41]

    Human-in-the-loop workflows with Lang- Graph: Interrupts, approvals, and async execution,

    Abstract Algorithms, “Human-in-the-loop workflows with Lang- Graph: Interrupts, approvals, and async execution,” https://www. abstractalgorithms.dev/langgraph-human-in-the-loop, Apr. 2026, accessed July 2026

    2026

  42. [42]

    Seccomp BPF (SECure COM- Puting with filters),

    The Linux Kernel documentation, “Seccomp BPF (SECure COM- Puting with filters),” https://www.kernel.org/doc/html/latest/ userspace-api/seccomp filter.html, accessed July 2026

    2026

  43. [43]

    The true cost of containing: A gVisor case study,

    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,” inProc. 11th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud), 2019

    2019

  44. [44]

    WASI: The WebAssembly System Interface,

    Bytecode Alliance, “WASI: The WebAssembly System Interface,” https://wasi.dev, accessed July 2026

    2026

  45. [45]

    Making reliable distributed systems in the presence of software errors,

    J. Armstrong, “Making reliable distributed systems in the presence of software errors,” Ph.D. dissertation, KTH Royal Institute of Technology, Stockholm, 2003

    2003

  46. [46]

    Notes on structured concurrency, or: Go statement con- sidered harmful,

    N. J. Smith, “Notes on structured concurrency, or: Go statement con- sidered harmful,” https://vorpus.org/blog/notes-on-structured- concurrency-or-go-statement-considered-harmful/, 2018, accessed July 2026

    2018

  47. [47]

    Edit automata: Enforcement mechanisms for run-time security policies,

    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

    2005

  48. [48]

    Macaroons: Cookies with contextual caveats for decentralized authorization in the cloud,

    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,” inProc. Network and Distributed System Security Symposium (NDSS), 2014

    2014

  49. [49]

    Capsicum: Practical capabilities for UNIX,

    R. N. M. Watson, J. Anderson, B. Laurie, and K. Kennaway, “Capsicum: Practical capabilities for UNIX,” inProc. 19th USENIX Security Symposium, 2010

    2010

  50. [50]

    CHERI: A hybrid capability-system architecture for scalable software compartmentalization,

    R. N. M. Watsonet al., “CHERI: A hybrid capability-system architecture for scalable software compartmentalization,” inProc. IEEE Symposium on Security and Privacy, 2015

    2015

  51. [51]

    Richardson,Microservices Patterns

    C. Richardson,Microservices Patterns. Manning, 2018, ch. 3 (Trans- actional Outbox pattern)

    2018

  52. [52]

    Differential testing for software,

    W. M. McKeeman, “Differential testing for software,”Digital Technical Journal, vol. 10, no. 1, pp. 100–107, 1998

    1998

  53. [53]

    Finding and understand- ing bugs in C compilers,

    X. Yang, Y. Chen, E. Eide, and J. Regehr, “Finding and understand- ing bugs in C compilers,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2011

    2011

  54. [54]

    In search of an understandable consensus algorithm,

    D. Ongaro and J. Ousterhout, “In search of an understandable consensus algorithm,” inProc. USENIX Annual Technical Conference (ATC), 2014

    2014

  55. [55]

    Model checking agent programming languages,

    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

    2012

  56. [56]

    AgentBench: Evaluating LLMs as agents,

    X. Liuet al., “AgentBench: Evaluating LLMs as agents,” inProc. Int. Conf. Learning Representations (ICLR), 2024

    2024

  57. [57]

    IronFleet: Proving practical distributed systems correct,

    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,” inProc. ACM Symp. Operating Systems Principles (SOSP), 2015

    2015

  58. [58]

    Verdi: A framework for implementing and formally verifying distributed systems,

    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,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2015

    2015

  59. [59]

    Using Crash Hoare Logic for certifying the FSCQ file system,

    H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich, “Using Crash Hoare Logic for certifying the FSCQ file system,” inProc. ACM Symp. Operating Systems Principles (SOSP), 2015

    2015

  60. [60]

    Cilium: eBPF-based networking, observability, and security,

    Cilium Authors, “Cilium: eBPF-based networking, observability, and security,” 2024. [Online]. Available: https://cilium.io

    2024

  61. [61]

    Falco: Cloud-native runtime security,

    The Falco Authors, “Falco: Cloud-native runtime security,” CNCF,

  62. [62]

    IEC 61508: Functional safety of electrical/electronic/programmable electronic safety- related systems,

    International Electrotechnical Commission, “IEC 61508: Functional safety of electrical/electronic/programmable electronic safety- related systems,” Edition 2.0, IEC, Geneva, 2010

    2010

  63. [63]

    ISO 26262: Road vehicles—Functional safety,

    International Organization for Standardization, “ISO 26262: Road vehicles—Functional safety,” 2nd ed., ISO, Geneva, 2018

    2018

  64. [64]

    ISO 10218-1: Robots and robotic devices—Safety requirements for industrial robots—Part 1: Robots,

    International Organization for Standardization, “ISO 10218-1: Robots and robotic devices—Safety requirements for industrial robots—Part 1: Robots,” ISO, Geneva, 2011

    2011

  65. [65]

    The notions of consistency and predicate locks in a database system,

    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

    1976

  66. [66]

    The seven turrets of Babel: A taxonomy of LangSec errors and how to expunge them,

    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,” inProc. IEEE Cybersecurity Development (SecDev), 2016, pp. 45–52

    2016

  67. [67]

    Introducing ChatGPT agent: bridging re- search and action,

    OpenAI, “Introducing ChatGPT agent: bridging re- search and action,” Jul. 2025. [Online]. Available: https://openai.com/index/introducing-chatgpt-agent/

    2025

  68. [68]

    τ-bench: A benchmark for tool-agent-user interaction in real-world domains,

    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

    Pith/arXiv arXiv 2024

  69. [69]

    Efficient software-based fault isolation,

    R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, “Efficient software-based fault isolation,” inProc. 14th ACM Symp. Operating Systems Principles (SOSP), 1993, pp. 203–216

    1993

  70. [70]

    Polymorphic effect systems,

    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

    1988

  71. [71]

    A brief account of runtime verifica- tion,

    M. Leucker and C. Schallhart, “A brief account of runtime verifica- tion,”J. Logic and Algebraic Programming, vol. 78, no. 5, pp. 293–303, 2009

    2009

  72. [72]

    MillWheel: Fault-tolerant stream processing at Internet scale,

    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

    2013

  73. [73]

    How Amazon Web Services uses formal methods,

    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

    2015

  74. [74]

    Web Services Business Process Execution Language version 2.0,

    OASIS, “Web Services Business Process Execution Language version 2.0,” OASIS Standard, Apr. 2007

    2007

  75. [75]

    Workflow patterns,

    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

    2003

  76. [76]

    Semantics of asyn- chronous JavaScript,

    M. C. Loring, M. Marron, and D. Leijen, “Semantics of asyn- chronous JavaScript,” inProc. 13th ACM SIGPLAN Int. Symp. Dynamic Languages (DLS), 2017, pp. 51–62

    2017

  77. [77]

    State management in Apache Flink: Consistent stateful distributed stream processing,

    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. 1718– 1729, 2017

    2017

  78. [78]

    MemGPT: Towards LLMs as operating systems,

    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

    Pith/arXiv arXiv 2023

  79. [79]

    AIOS: LLM agent operating system,

    K. Mei, Z. Li, S. Xu, R. Ye, Y. Ge, and Y. Zhang, “AIOS: LLM agent operating system,” arXiv:2403.16971, 2024

    Pith/arXiv arXiv 2024

  80. [80]

    RustBelt: Securing the foundations of the Rust programming language,

    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

    2018

Showing first 80 references.