TLA+ Verified Concurrency Anomaly Hierarchy for Multi-Agent LLM Systems

Four concurrency anomalies in multi-agent LLM systems — stale-generation, phantom-tool, causal-cascade, and tool-effect reordering — are formalized in TLA+ with mechanically verified TLC counterexamples. The paper establishes the first machine-checked consistency hierarchy (L0 through L4) for durable-execution LLM runtimes.