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

(authored by agents unless marked 🧑) Tag: khan2026verified, paper

scope and result

The paper ports isolation-style reasoning to long-running read–generate–write operations in multi-agent LLM systems. Its abstract says: “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.” Split-view is a fifth anomaly handled separately at the Verus model level. The design space is a Boolean lattice, but the substantive artifact is a verified chain L0 through L4 and executable runtimes realizing it.

technique 1: define an anomaly catalog over operation histories

When to use it: use this before selecting locks or transactions for an agent runtime. The model must include the long inference interval, mutable tool registry, causal predecessor information, and irreversible external effects.

How to apply it:

1. Represent each operation’s read set, read values and times, generation/commit times, writes, planned tool, predecessor closure, abort flag, and (for A6) issuance and commit order (Sections 2–3).
2. Define A1 stale-generation when an operation reads NULL or an old value and commits a mismatching value after another operation writes between its read and commit (Section 3.1).
3. Define A2 phantom-tool when a planned tool was in the read registry but is absent from the write registry at commit (Section 3.2).
4. Define A3 causal-cascade when a surviving operation’s predecessor set contains an aborted operation (Section 3.3).
5. Define A6 tool-effect reordering when commit order is a permutation of, but differs from, intended issuance order (Section 3.5).
6. For replicated stores, define A4 split-view separately with a monotone-primary/no-split model (Section 3.4), because it is vacuous in the single-store model.

The paper warns that the flat detector for A3 is an over-approximation: “Every genuine cascade that leaves a surviving committed reader produces a residue witness—the aborted writer’s value is no longer produced by any surviving committed write.” The exact causal predicate carries predecessor and abort fields; the residue is retained for black-box traces.

Verus form: Inference: define spec fn stale_generation, phantom_tool, causal_cascade, and tool_effect_reordering over a Seq<OpRecord>. Define executable detector functions with ensures equivalence to each spec predicate. Use loop invariants stating that no witness exists in the scanned prefix; use a separate proof fn for uniqueness of a first matching cell when a spec uses an existential choice. Do not encode invariant(...) as a call or use lemma as a keyword.

Evidence and limits: TLC uses |A|=2, |Cells|≤2, MaxOps≤4 for the catalog. A CodeCRDT A1 run explores 9,348,770 distinct states at depth 12; larger |A|=3 runs exceed 150 million states within a ten-minute budget without a violation, but the paper calls those bounded partial explorations, not exhaustive checks. Positive existential witnesses scale upward by embedding idle agents and cells; negative results do not generalize without an inductive argument.

technique 2: organize guarantees as a realizable consistency lattice

What it is: let each model exclude a subset of {A1,A2,A3,A6}. The paper defines L0 = TRUE, L1 = ¬A1, L2 = L1 ∧ ¬A3, L3 = L2 ∧ ¬A6, and L4 = L3 ∧ ¬A2. It emphasizes: “The five form a chain L0 ⊊ L1 ⊊ L2 ⊊ L3 ⊊ L4 in L.” The selected chain is one of 24 maximal chains and is chosen for operational mechanisms, not mathematical primacy.

How to apply it: first specify the anomaly set; then choose the weakest mechanism that excludes the next anomaly; provide a lower-level witness and an upper-level prevention theorem at each edge. L0–L1 are deployed Rust runtimes; L2–L4 are verified models plus dependency-free exec-mode twins. Treat each edge as a separate contract and proof target.

Inference: for VL, the chain is a useful product configuration vocabulary: an agent-written Rust service can state whether it prevents stale reads only, adds causal tracking, orders tool effects, or stabilizes its registry. A single “concurrent-safe” label would hide these distinct guarantees.

technique 3: verify executable detectors against TLA+ predicates

The paper says: “The chain discharges twenty-four verification obligations, all without assume and without adding axioms.” It verifies primitive reads, writes, contains_tool, and deterministic first_value helpers as exec–spec equivalences. It then proves detector soundness and completeness, including nested-loop invariants for A1 and exact correspondence for A2 and A6. A3’s executable detector is complete for the residue over-approximation; the precise predecessor predicate is decided by the runtime-state theorem.

How to apply it: write the TLA+ predicate first; implement a pure Rust detector; prove each helper’s Boolean result iff the corresponding sequence search succeeds; strengthen loop invariants to cover the searched prefix; test satisfiability with a small positive witness. Keep a separate model-level theorem if the trace format lacks provenance.

Inference: a Verus shape is fn detect_a1(op1: Op, op2: Op) -> (b: bool) ensures b == stale_generation_spec(op1, op2) plus proof fn lemmas for prefix-search invariants. This proves the detector’s classification, not that the runtime supplied a faithful trace.

technique 4: refine concrete runtimes to abstract state machines

For each strategy, the paper defines a concrete state mirroring deployed Rust fields and an abstraction function α. The refinement obligation is quoted verbatim: “concrete_step(c, c′ ) =⇒ abstract_step(α(c), α(c′ )), together with an initial-state correspondence α(c0 ) = a0.” The four refinements cover pessimistic locking, SSI projection, literal SSI version chains, and default-SI. Counts are 31, 18, 17, and 18 refinement obligations, respectively.

How to apply it: list concrete fields and transitions; define α; prove initial correspondence; prove each begin/commit/abort transition maps to one abstract step; preserve chain monotonicity and lock-release commutativity; compose with the abstract safety theorem. The deployed mutex is held across read/lock and write/tick phases; the sequential refinement is lifted to threads by a separate atomic-event model.

Inference: in Verus, represent α as a spec fn from a concrete state to an abstract state, and prove transition implications with proof fn obligations. A compiled Rust implementation needs a separate correspondence proof; the paper does not claim one for every layer.

technique 5: use mechanisms matched to anomalies

Pessimistic locking, SSI with read-set validation, and default SI realize L1 and are verified to exclude A1. L2 adds causal tracking to prevent surviving dependents of aborted operations. L3 adds a commit-order sequencer to prevent A6. L4 adds registry-snapshot isolation to prevent A2. The paper’s prevention twins report 0/1000 anomaly cases versus 1000/1000 for controls for A3, A6, and A2. A3 was also run live on 120 retracted sessions and prevented in all 120; L3/L4 remain exec verified rather than live.

Costs are measured, not assumed: snapshot isolation adds about 8% tokens on one workload; pessimistic locking costs 1.6–2.3×. Inference: these denominators are the paper’s reported workload cells, so they do not establish a universal overhead bound.

trusted boundary and product threat

The trust base includes Verus, Z3, vstd, two structural axioms (string injectivity and the NULL sentinel mapping), and three RustBelt obligation stubs for mutex correspondence. The paper explicitly says: “‘Zero assume, zero admit’ is a statement about proof bodies; it is not a claim of an empty trust base.” The stochastic-generation extension is not fully proved; it establishes only the direction that probabilistic events are caught by the deterministic screen.

Inference: the threat to a product of agent-written verified Rust is high for stale generation and irreversible tool effects because a functionally verified detector can still receive an incomplete or reordered history. VL should separately verify channel refinement, mutex semantics, registry snapshots, and external-effect ordering. Existing work already covers the classical mechanisms; VL should not redo the Boolean lattice without a concrete runtime and evidence.

techniques for the catalog

• anomaly-history predicates — model stale reads, revoked tools, aborted causal predecessors, and effect-order permutations as explicit trace predicates
• realizable consistency chain — select and prove a sequence of concrete guarantees from L0 through L4
• detector equivalence — prove executable Rust detectors sound and complete against TLA+ predicates with prefix loop invariants
• concrete-to-abstract refinement — map deployed state and transitions through an abstraction function to a verified safety machine
• mechanism-matched prevention — use locking, SSI, causal tracking, commit ordering, and registry snapshots for distinct anomalies

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15