# Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems

arXiv: https://arxiv.org/abs/2606.17182 · HTML: https://mlsanity.com/paper/2606.17182/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 22 of its 96 references that are in the map.
- First posted on arXiv 15 Jun 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 22 of 22)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Generative Agents: Interactive Simulacra of Human Behavior](https://mlsanity.com/paper/2304.03442/) (2023)
- [AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation](https://mlsanity.com/paper/2308.08155/) (2023)
- [MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework](https://mlsanity.com/paper/2308.00352/) (2023)
- [MemGPT: Towards LLMs as Operating Systems](https://mlsanity.com/paper/2310.08560/) (2023)
- [Gorilla: Large Language Model Connected with Massive APIs](https://mlsanity.com/paper/2305.15334/) (2023)
- [Why Do Multi-Agent LLM Systems Fail?](https://mlsanity.com/paper/2503.13657/) (2025)
- [Efficient Guided Generation for Large Language Models](https://mlsanity.com/paper/2307.09702/) (2023)
- [The Good, The Bad, and The Greedy: Evaluation of LLMs Should Not Ignore Non-Determinism](https://mlsanity.com/paper/2407.10457/) (2024)
- [SagaLLM: Context Management, Validation, and Transaction Guarantees for Multi-Agent LLM Planning](https://mlsanity.com/paper/2503.11951/) (2025)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Atomix: Timely, Transactional Tool Use for Reliable Agentic Workflows](https://mlsanity.com/paper/2602.14849/) (2026)
- [CodeCRDT: Observation-Driven Coordination for Multi-Agent LLM Code Generation](https://mlsanity.com/paper/2510.18893/) (2025)
- [Verification-Aware Planning for Multi-Agent Systems](https://mlsanity.com/paper/2510.17109/) (2025)
- [Elle: Inferring Isolation Anomalies from Experimental Observations](https://mlsanity.com/paper/2003.10554/) (2020)
- [Verifying Strong Eventual Consistency in Distributed Systems](https://mlsanity.com/paper/1707.01747/) (2017)
- [Highly Available Transactions: Virtues and Limitations (Extended Version)](https://mlsanity.com/paper/1302.0309/) (2013)
- [Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs](https://mlsanity.com/paper/1601.01001/) (2016)
- [Stateless Model Checking for TSO and PSO](https://mlsanity.com/paper/1501.02069/) (2015)
- [Consistency in Non-Transactional Distributed Storage Systems](https://mlsanity.com/paper/1512.00168/) (2015)

## Built on by (most cited first, 8 of 8)

- [MemTX: Transactional Belief Commit for Stateful Agent Memory](https://mlsanity.com/paper/2607.23929/) (2026)
- [Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives](https://mlsanity.com/paper/2607.14166/) (2026)
- [Graph Engineering in the Era of LLM Agents: From Individual Intelligence to System Intelligence](https://mlsanity.com/paper/2608.21156/) (2026)
- [Beyond Corrected Memory: Execution Consistency in Multi-Agent Systems](https://mlsanity.com/paper/2610.08101/) (2026)
- [When Tool Calls Succeed but Workflows Fail: Anomalies at the Agent-Tool Boundary](https://mlsanity.com/paper/2609.15397/) (2026)
- [LeaseGuard: Incumbent-Preserving Admission Control for Privileged LLM Agents](https://mlsanity.com/paper/2609.24077/) (2026)
- [When Evidence Changes: Evaluating Memory Repair and Re-reading in Language-Model Agents](https://mlsanity.com/paper/2610.03902/) (2026)
- [When Agent Context Goes Stale: Incoherence in Volatile Agent Context](https://mlsanity.com/paper/2610.05281/) (2026)

## Abstract (arXiv)

Multi-agent LLM systems share state through memory stores, vector indices, and tool registries. We model such sharing as long-running read-generate-write operations under deterministic-generation semantics -- the regime durable-execution engines enforce by deterministic replay -- and formalize four concurrency anomalies in TLA+: stale-generation, phantom-tool, causal-cascade, and tool-effect reordering, structural analogues of classical isolation anomalies, each with a TLC counter-example. The exclusion lattice over these anomalies is trivial; the contribution is the mechanically verified realizability and strict separation of one maximal chain within it, L0 subsetneq cdots subsetneq L4, to our knowledge the first machine-checked consistency hierarchy for such runtimes. A development of 274 Verus obligations (zero assume, zero admit; trust base: two structural axioms and a mutex correspondence) proves the detectors sound and complete against the specifications and each runtime its avoidance set. Three deployed Rust runtimes realize L0-L1 (pessimistic locking, serializable snapshot isolation, default-SI), each verified against stale-generation and refined to its state machine; L2-L4 are exec-mode-verified with dependency-free prevention twins (A3, A6, A2: 0/1000 versus 1000/1000), and L2 is run live across three model families (A3 prevented in all 120 retracted sessions). We reproduce a silent lost update in ByteDance's deer-flow, formalizing its fix as a verified L0 → L1 refinement, and exhibit tool-effect reordering in LangGraph's ToolNode on unmodified output, removed by an L3 commit-order sequencer. The verified detector, refinements, and realizability artifacts are the contribution; the phenomena and lattice are classical.