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

这篇论文把多 Agent LLM 系统共享 memory store、vector index、tool registry 的过程建成 read-generate-write 操作，并用 TLA+ 给出 stale-generation、phantom-tool、causal-cascade、tool-effect reordering 四类并发异常的可执行规格。它的技术硬度在于 274 个 Verus 证明义务全部以 zero assume、zero admit 完成，并把 L0 到 L4 的一致性层级映射到可验证 runtime。作者还复现 ByteDance deer-flow 的 silent lost update，并展示 LangGraph ToolNode 的 tool-effect reordering 可由 L3 commit-order sequencer 消除；这让 Agent harness 的“并发正确性”从经验 bug 进入可检查设计空间。