New paper formally verifies concurrency safety in multi-agent LLM systems

A new paper from Sajjad Khan tackles the growing problem of concurrency bugs in multi-agent LLM systems. As multiple AI agents share memory stores, vector indices, and tool registries, they can encounter anomalies analogous to classic database isolation issues. The paper formalizes four specific anomalies—stale-generation (reading outdated state), phantom-tool (inconsistent tool results), causal-cascade (cascading stale updates), and tool-effect reordering (non-serializable tool side-effects)—using TLA+ and models them as long-running read-generate-write operations.

The contribution is a mechanically verified consistency hierarchy (L0 ⊊ ... ⊊ L4) using 274 Verus obligations with zero assumptions (only two structural axioms and a mutex correspondence). The author provides three verified Rust runtimes implementing L0–L1 (pessimistic locking, serializable snapshot isolation, default-SI) and exec-mode-verified prevention for L2–L4. Practical impact includes reproducing a silent lost update in ByteDance's deer-flow (fixed via L0→L1 refinement) and demonstrating tool-effect reordering in LangGraph's ToolNode (removed by an L3 commit-order sequencer).