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

Sajjad Khan

Source-linked AI summary

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

Sajjad Khan

arXiv:2606.17182v1Jun 15, 2026cs.LGcs.DCcs.LOcs.MAcs.PL

TL;DR

Multi-agent LLM runtimes lack mechanically verified evidence about which concurrency anomalies are realizable and how prevention mechanisms separate consistency levels. This paper formalizes and verifies four anomalies, their detectors, runtime refinements, and a strict L0–L4 chain, establishing mechanically verified realizability and separation.

Problem
Existing work does not settle which concurrency-anomaly combinations are realizable by concrete runtimes or separated by verified prevention theorems.
Method
The paper formalizes four anomalies and a consistency chain in TLA+, then verifies detector soundness, completeness, runtime refinements, and prevention disciplines in Verus and TLAPS.
Results
The verified artifacts establish realizability and strict separation of the L0–L4 chain, including deployed-runtime refinements and prevention of reproduced deer-flow and LangGraph anomalies.
Takeaways & Limitations
The work provides a machine-checked consistency hierarchy and verified runtime mechanisms for analyzing and preventing concurrency anomalies in multi-agent LLM systems.
Takeaways & Limitations
The deterministic stale-generation predicate does not fully refine the operational notion of disagreement under stochastic generation, so the paper treats this as a scope separation.

Abstract

from arXiv · show

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, $L_0 \subsetneq \cdots \subsetneq L_4$, 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 $L_0 \to L_1$ 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.

1 INTRODUCTION

The paper presents a mechanically verified consistency hierarchy for concurrency anomalies in multi-agent LLM systems, emphasizing verified detectors, runtime guarantees, and deployed refinements rather than the catalog or lattice itself. It also demonstrates practical relevance through a reproduced deer-flow lost update and live L2 prevention results.

Deployed relevance: A reproduced silent lost update in ByteDance’s deer-flow is formalized as a verified L0→L1 refinement, establishing a deployed instance of the lattice’s base anomaly.The paper distinguishes this live production issue from its constructed motivating scenario.
Anomaly catalog: Four anomalies—stale-generation, phantom-tool, causal-cascade, and tool-effect-reordering—are formalized in TLA+ and each has a TLC counter-example trace.The catalog also identifies split-view, which requires replication and falls outside the single-store operational model.
Consistency hierarchy: The Boolean lattice has sixteen points, with five distinguished levels L0,...,L4 selected along one operationally motivated maximal chain.The chain is one of twenty-four linear extensions, not mathematically privileged.
Mechanized verification: Verus proves the four detector implementations sound and complete against their TLA+ specifications, while three deployed runtimes are verified safe against A1.The detector pipeline discharges 24 obligations; runtime proofs cover pessimistic locking, SSI, and default-SI, with default-SI conditional on an all-writers workload hypothesis.
Deployment scope: The deployed runtimes implement only L0→L1, whereas L2–L4 are represented by separate verified runtime models rather than claimed as pilot-runtime capabilities.The higher-level artifacts use causal tracking with cascading abort, saga compensation, and registry-snapshot isolation.
Live validation: 0/1000 versus 1000/1000 demonstrates the L2 causal-tracking twin’s A3 prevention, and the live runtime prevents A3 in all 120 retracted sessions across three model families.Supervisors retract plans at 0%, 15.5%, and 44.5% on the triage workload.

2 BACKGROUND AND RUNTIME MODEL

The paper models multi-agent LLM systems as concurrent, long-running read–generate–write operations over shared memory and a tool registry. The model deliberately limits scope through deterministic generation, record-level internal atomicity, and other simplifications for formal tractability.

Operational model: Each operation reads selected memory cells and registry contents, performs a non-instantaneous generation phase, then atomically appends writes and tool metadata to an operation log.The append-only log length serves as the logical clock.
Model scope: The framework targets long-running concurrent operations under inference-bounded latency, while acknowledging that deployed runtimes use heterogeneous abstractions and do not directly mirror this model.The paper motivates the model by exhibiting placements of contemporary runtimes, while noting that mapping them is non-trivial.
Scope limitations: The model uses a single logical shared store without replication, and its simplifications are deliberate concessions to formal tractability that define the scope of the results.Replicated stores would introduce split-view anomalies requiring a richer model.
Model assumptions: LLM invocations are treated as deterministic in their inputs, so generated writes and tool calls depend on read values and tools visible at read time.This assumption defines the operational-claims boundary, whereas the mechanized results themselves range over recorded histories with write values free.
Atomicity assumptions: Internal shared-store state commits atomically at the OpRecord level, but external tool effects may occur before the record’s store update and therefore need not preserve the same ordering.This two-layer atomicity distinction is the basis for formalizing the tool-effect gap as A6.

3 THE ANOMALY CATALOG

The catalog formalizes four concurrency anomalies—stale-generation, phantom-tool, causal-cascade, and tool-effect reordering—while deferring split-view from the single-store model. Each formalized anomaly is defined over operation histories and accompanied by a TLC-verified witness.

Catalog scope: Four anomalies are formalized as history predicates, with TLC witnesses reproduced in the supplementary artifact; split-view is deferred.The catalog’s TLC runs use |A| = 2 agents, |Cells| ≤2 memory cells, and MaxOps ≤4.
Stale-generation: Stale-generation occurs when an operation commits after another agent writes a value differing from its earlier read during generation.TLC produces a five-state witness at |A| = 2, |Cells| = 1, MaxOps = 4: 0 < 1 < 2 and NULL ≠ v1.
Phantom-tool: Phantom-tool occurs when a planned tool is removed during generation and the operation commits a call to that absent capability.TLC produces a four-state witness at |A| = 2, |Tools| = 2, MaxOps = 3.
Causal-cascade: Causal-cascade occurs when a surviving non-aborted operation retains an aborted predecessor in its causal closure, and L2 prevents this predicate mechanically.Theorem L2h establishes absence on every reachable L2 state with no assume/admit, while L2g establishes non-vacuity.
Split-view: Split-view is vacuous in the single-store model because formalizing replicated divergent reads would require replica identifiers, synchronization transitions, and visible-replica sets.It is formalized separately rather than distinguishing a lattice point solely by its prevention.

4 THE CONSISTENCY LATTICE · 4.1 Five distinguished points: the Ln chain

The paper models consistency levels as subsets of four excluded anomalies, forming a 16-element Boolean lattice. It distinguishes five named points that form the strict chain L0 ⊊ L1 ⊊ L2 ⊊ L3 ⊊ L4.

4 THE CONSISTENCY LATTICE: A consistency model is characterized by the anomalies it excludes from operation histories.Each subset of A = {A1,A2,A3,A6} defines a model that excludes exactly those anomalies and admits the others.
4 THE CONSISTENCY LATTICE: 16 elements comprise the Boolean lattice of consistency models.The lattice is L = ⟨2^A,⊆⟩, with bottom ⊥ = ∅ admitting all anomalies.
4.1 Five distinguished points: the Ln chain: Five named points are selected along the lattice.These points are introduced as the distinguished levels developed in the following subsection.
4.1 Five distinguished points: the Ln chain: The five points form the strict chain L0 ⊊ L1 ⊊ L2 ⊊ L3 ⊊ L4.The chain is ordered by progressively stronger predicates over operation histories.
4.1 Five distinguished points: the Ln chain: The practitioner-facing TLA+ representation of the five points appears in Listing 1.The listing presents the definitions as they occur in Levels.tla.
4.1 Five distinguished points: the Ln chain: The TLA+ definitions add exclusions cumulatively from L0 through L4.L0 is TRUE; L1 excludes stale-generation, L2 additionally excludes causal-cascade, L3 additionally excludes tool-effect reordering, and L4 additionally excludes phantom-tool.

4.2 One linearization among twenty-four · 4.3 What is and is not trivial: the realizability frontier

The paper treats the Boolean lattice as mathematically trivial and focuses instead on the realizability frontier: which anomaly combinations are inhabited, implementable, and strictly separated. It selects one operationally motivated maximal chain and mechanically verifies concrete runtime realizations along it.

4.2 One linearization among twenty-four: 4! = 24 maximal chains linearly extend the Boolean lattice, and each visits the bottom, one node per cardinality layer, and the top.All maximal chains are mathematically equivalent.
4.2 One linearization among twenty-four: The chosen A1 → A3 → A6 → A2 ordering is operational rather than canonical, beginning with the weakest non-trivial staleness guarantee.A1 represents the basic read–generate–write staleness failure.
4.2 One linearization among twenty-four: The eleven off-chain lattice points represent anomaly combinations not directly targeted by the operational pilot but remain accessible to the same verification machinery.They are candidates for future work through alternative chains.
4.3 What is and is not trivial: the realizability frontier: The substantive contribution is the realizability frontier, not the Boolean algebra itself: determining which points correspond to genuine anomalies, concrete runtime mechanisms, and separable guarantees.The lattice has four generators and sixteen points.
4.3 What is and is not trivial: the realizability frontier: 24 detector obligations establish mechanical soundness and completeness against the TLA+ predicates, with no assume, no added axiom.The same core also includes unconditional verification of the SSI runtime’s ¬A1 property and the L2 refinement’s zero added axioms.
4.3 What is and is not trivial: the realizability frontier: Each anomaly generator has an explicit TLC counter-example, while the selected chain names implementable mechanisms whose avoidance-set mapping supplies the design content.The mechanisms include pessimistic locking, serializable snapshot isolation with causal tracking, and saga compensation.
4.3 What is and is not trivial: the realizability frontier: L1, L2, L3, and L4 each have a Verus safety theorem, a strict refinement witness, and a concrete runtime that adds one prevented anomaly.L0 and L1 use deployed, executable Rust runtimes; L2–L4 additionally use exec-mode artifacts with dependency-free twins measured at 0/1000 versus 1000/1000.

4.4 Visualization and the lattice table · 4.5 The snapshot-insufficiency observation

The chosen consistency chain is visualized within a sixteen-point lattice and tabulated by anomaly admissions and preventions. A TLC-verified witness shows that a generation snapshot alone does not exclude stale-generation, motivating L1’s explicit read-set stability condition.

4.4 Visualization and the lattice table: The diagram highlights the chosen L_n chain in bold, while Table 2 tabulates its anomaly behavior.Together, the visualization and table identify the selected hierarchy’s structure and anomaly status.
4.4 Visualization and the lattice table: The Hasse diagram contains 16 lattice points and 32 cover edges, with the selected chain highlighted among 24 maximal chains.The eleven unnamed points represent variants reachable through alternative linearizations.
4.4 Visualization and the lattice table: Table 2 records each named chain point’s verified admissions and mechanical preventions for all four formalized anomalies.Admissions use explicit TLC counterexamples, while preventions follow definitions and a TLAPS coherence check.
4.5 The snapshot-insufficiency observation: A structural snapshot alternative is defined to formalize reads reflecting memory values at their read time.The observation addresses why L1 includes explicit ¬A1 rather than relying solely on a snapshot guarantee.
4.5 The snapshot-insufficiency observation: TLC verifies a history where Lstruct_1 holds while StaleGeneration remains true.Thus, the structural snapshot condition does not exclude A1.
4.5 The snapshot-insufficiency observation: 1,934 states at depth 5 suffice for TLC to find the witness with |A| = 2, |Cells| = 1, and MaxOps = 3.The same 5-state witness reproduces for |A| = 3 and MaxOps ∈ {6,9}.
4.5 The snapshot-insufficiency observation: In the witness, a2 commits a stale read after a1’s intervening write, although the snapshot condition held at a2’s read time.L1 rejects this single-sided staleness by adding explicit read-set stability; broader structural insufficiency remains open.

4.6 TLAPS consistency check on chain definitions · 4.7 Spec–implementation equivalence in Verus

TLAPS checks the chain definitions through definitional unfolding but provides only textual coherence. Verus instead mechanically proves executable detectors equivalent to their specifications, including 24 obligations discharged without assumptions or added axioms.

4.6 TLAPS consistency check on chain definitions: TLAPS decomposes eleven chain theorems into 15 obligations, all discharged by definitional unfolding.The theorems cover adjacent containments, transitive soundness, and one aggregate result.
4.6 TLAPS consistency check on chain definitions: The TLAPS check constrains stalegeneration-free executions through read-set stability or value agreement, under two trace-lifted invariants.The invariants are single-operation-in-flight and read-before-write monotonicity.
4.7 Spec–implementation equivalence in Verus: TLAPS establishes well-typed anomaly predicates and the chain’s refinement order, but is explicitly a textual-consistency check rather than a correctness argument.The substantive mechanization is the Verus chain.
4.7 Spec–implementation equivalence in Verus: Verus discharges 24 verification obligations without assume and without adding axioms.These obligations support the link between formal predicates and executable detectors used in the empirical pilot.
4.7 Spec–implementation equivalence in Verus: Primitive reads, writes, and tool-membership operations are verified as sound and complete exec–spec equivalences.The equivalences range over read sets, write sets, and tool sequences.
4.7 Spec–implementation equivalence in Verus: first_value_exec agrees with a deterministic first-match specification, enabled by a uniqueness lemma for the matching index.The lemma makes the existential witness well-defined under Verus’s choose semantics.
4.7 Spec–implementation equivalence in Verus: The four executable detectors are mechanically equivalent to their formal anomaly predicates through soundness and completeness proofs.Unlike TLAPS unfolding, these proofs require nested-quantifier reasoning and loop invariants covering searched prefixes.

4.8 Spec–runtime refinement in Verus

Section 4.8 closes the gap between verified abstract state machines and deployed Rust runtimes through four Verus refinement proofs. Concrete executions map to abstract executions satisfying ¬A1, under sequential semantics lifted to multithreading by mutex correctness.

Refinement structure: Four Verus refinements map deployed Rust states and transitions to abstract pessimistic-locking, SSI, and default-SI state machines, preserving initial-state correspondence.Each strategy uses a concrete state record, abstraction function α, and transition-lifting lemmas.
Refinement result: Every concrete execution maps to an abstract execution satisfying ¬A1.This follows by composing initial-state correspondence and transition refinements with the abstract safety theorems.
Trust base: The refinement trust base contains two structural axioms: string-identifier injectivity and mapping the concrete NULL sentinel to abstract value 0.A finite-map preservation candidate is instead proven as a Verus lemma, not trusted as an axiom.
Scope of refinement: The four refinements are sequential, while a mutex held across begin and commit lifts the correspondence to multithreaded execution.The refinement models one logical operation at a time; mutex correctness supplies the concurrency lift.
Combined formal scorecard: 84 verified obligations cover the four refinement files, with zero assume and zero admit.The combined scorecard reports all counts as live-confirmed by verus_count.sh.

4.9 Probabilistic refinement of A1

Under stochastic generation, deterministic A1 string comparison can over-approximate operational stale-read disagreement. The probabilistic refinement defines disagreement by counterfactual downstream behavior, but establishes only one-way screening soundness rather than complete safety detection.

Probabilistic refinement of A1: Under stochastic generation, string inequality does not necessarily imply operational stale-read disagreement, although string equality forces operational equivalence under identical inputs.A fresh re-read may produce the same downstream output despite differing recorded strings.
Probabilistic refinement of A1: The refinement introduces disagreement_probability as the percentage chance that observing a fresh value would change an agent’s downstream output.The specification leaves this function uninterpreted and estimates it by rerunning the prompt with the fresh value substituted.
Probabilistic refinement of A1: k ≥100 supports the specification-level claim that an empirical estimator at an inflated threshold soundly implies true probabilistic detection.The over-approximation chain is not a mechanized proof, and the direction is unsuitable as a complete safety screen.
Probabilistic refinement of A1: The deterministic detector catches every probabilistic event, but not conversely, because differing strings can yield identical downstream outputs.Thus it is a sound candidate-anomaly screen, conditional on axiom (b), but does not guarantee that every operationally real A1 event is observed.

4.10 Concurrent semantics lift

The section lifts sequential refinements to a mechanized atomic-event model and mechanically verifies the L1→L2 step. The L2 runtime prevents causal-cascade anomalies through causal-closure tracking, with detector-level projection established, while executable refinement remains open above L1.

Concurrent semantics lift: The concurrent semantics model represents mutex execution as enabled LockAcquire, LockRelease, Read, and Write events, closing the sequential-interleaving gap.The model reports 9 verified, 0 errors, and 0 axioms.
L2 safety: causal-tracking runtime prevents A1 ∧A3: The L2 runtime records each transaction’s committed predecessors and accepts commits only when reads are fresh and all causal predecessors remain committed and non-aborted.Aborts cascade to every transaction that depends on the aborter, operationalizing serializable snapshot isolation with cascading abort.
L2 safety: causal-tracking runtime prevents A1 ∧A3: 22 verified theorems establish no A1/A3 at commit, sufficient one-level cascading abort through causal closure, satisfiable exclusions, and absence of A3 across reachable executions.The causal-closure invariant is inductive with five preservation lemmas, requiring no assume or admit.
L2 safety: causal-tracking runtime prevents A1 ∧A3: Every reachable committed read has a surviving committed producer for exactly its value, and projection theorems connect runtime states to detector-clean emitted histories.The projection closes the state-machine versus emitted Seq⟨OpRecord⟩ correspondence gap; projection verification reports 3 verified, 0 errors, 0 axioms, 0 external_body, and 0 assume.
L2 safety: causal-tracking runtime prevents A1 ∧A3: L2 is not yet refined to an executable Rust runtime; L3 and L4 instead receive dedicated runtime models in later sections.This residual is shared by every level above L1.

4.12 A4 split-view formalization

The section formalizes A4 split-view using an append-only, monotone-versioned primary and proves that fixed-version primary reads cannot disagree. It shows that genuine A4 arises from secondary lag, which read-from-primary pinning removes, while limiting the result to single-cell, single-primary replication.

Construction: The model uses an append-only, monotone-versioned primary log and records each read’s replica, version, value, and trace position.Primary reads observe the head; lagging secondaries may serve older log indices.
Scope: 9 verified theorems, 0 errors, 0 axioms, 0 external_body, and 0 assume support the formalization.The result covers a single cell and single primary; eventually consistent and CRDT-merge strategies remain out of scope.
Verified theorems: Append-only invariants prove that primary head versions are monotone and equal head versions imply identical logs.These lemmas are established by induction on the execution trace.
Verified theorems: Two primary reads at the same version observe the same value, so primary reads cannot produce split view at a fixed committed version.The safety result follows from append-only monotonicity rather than the predicate’s arity.
Verified theorems: A concrete lagging-secondary trace serves NULL at log index 0 while the primary serves 10 at version 1, producing a genuine A4 witness.The values are computed from model state, demonstrating non-vacuity.

4.13 Probabilistic case: a soundness-only screen, and the open concentration bound

The paper separates exact per-trace stale-read detection from the unproved distributional question of estimating divergence rates. A quantitative probabilistic refinement remains open because the current Verus toolchain lacks the real-number probability theory needed for a Hoeffding-grade concentration bound.

Per-trace detection: The deterministic detector is sound and complete for deciding whether a stale read occurred in a given execution trace.It fires iff a read observes a value differing from a later committed write on the same cell, with no false-negative concern for this trace property.
Scope separation: The distributional question—whether re-executing a read–generate–write window diverges—remains distinct from the exact per-trace question.The paper explicitly avoids claiming a probabilistic refinement among its contributions.
Open concentration bound: k = O((1/ε^2)log(1/δ)) samples are required for the stated ε,δ accuracy guarantee, but the current Verus distribution cannot mechanize the needed concentration proof.A Markov-style count bound is too weak to establish a Hoeffding-grade concentration guarantee, so no probabilistic refinement is claimed.

4.14 RustBelt interface specification

The section relocates the concurrency-semantics trust base to a precise std::sync::Mutex Acquire/Release correspondence, while subsequent verified L3 and L4 runtimes prevent tool-effect reordering and phantom-tool anomalies. Together, these results mechanically realize the strict chain L0 ⊊ L1 ⊊ L2 ⊊ L3 ⊊ L4.

4.14 RustBelt interface specification: The concurrency-semantics lift makes std::sync::Mutex conformity to the abstract Acquire/Release protocol the residual safety trust base.Four Verus theorems specify this interface, while lock_is_acquire, drop_is_release, and event_seqcst remain deliberately unproved stubs.
4.15 L3 safety: saga-compensation runtime prevents A6: L3 prevents A6 by combining causal tracking with saga compensation, whose verified composition prevents A1 ∧A3 ∧A6.The saga records ordered external calls, serializes issuance and completion, and compensates completed calls in reverse issuance order.
4.15 L3 safety: saga-compensation runtime prevents A6: The L3 commit-order sequencer prevents A6 for genuinely concurrent effects by externalizing effect k only after effects 0,...,k complete.The theorem was verified with 5 verified, 0 errors, 0 axioms, 0 external_body, and 0 assume, under arbitrary completion schedules including reversal.
4.16 L4 safety: registry-snapshot isolation prevents A2: L4 prevents A2 through validated commits or pinned-snapshot resolution, even when registry entries are removed or signatures change.The verified prevention theorems establish both disciplines, while a constructive witness shows A2 without either discipline.
4.16 L4 safety: registry-snapshot isolation prevents A2: Applying L2 causal tracking, L3 saga discipline, and L4 registry isolation prevents A1, A2, A3, and A6 simultaneously, mechanically closing L0 ⊊L1 ⊊L2 ⊊L3 ⊊L4.The model-level proofs establish sufficiency; live registry hot-swapping and related recovery remain engineering rather than re-verified details.

5 EMPIRICAL PILOT

The empirical pilot validates end-to-end detector operation on real LLM traces and shows that anomaly rates are primarily workload-engineered. Across measured runtimes, snapshot isolation prevents A1 with little detectable cost, while pessimistic locking eliminates A1 with bounded, workload-dependent overhead.

Pilot methodology: The detector pipeline runs end-to-end on real LLM traces, producing a level classification for each session under the selected chain.The approximately 200-line Python instrumentation exposes begin/commit snapshots and emits operation records aligned field-for-field with Memory.tla.
Workload sensitivity: A1 rates span 1%–100% across workloads, with workload structure dominating variation rather than demonstrating prevalence in unmodified production systems.The three workloads yield edit-review 100%, plan-execute 1%, and triage 35%; these are sensitivity checks of detector discrimination.
Runtime results: Every cell of Table 4 shows zero A1 instances under pessimistic locking, which drops conflicting operations before invoking the LLM beyond planning.The lock is acquired before reading, and failed acquisition silently drops the operation.
Runtime costs: ∼8% token overhead is the paired-design estimate for SSI on plan-execute, while between-session comparisons detect no SSI overhead versus vanilla.The paired estimate is statistically significant (p=0.007, 90% CI up to ∼12.6%), whereas confidence intervals overlap in every between-session cell.
Runtime costs: ≈62% is the measured triage increase for pessimistic locking, while worst-case overhead remains bounded at ≤1.6 × vanilla on gpt-4o.Pessimistic overhead is statistically zero on edit-review and plan-execute but real and significant on triage; measured overhead is governed by contention and abort rate.

6 DISCUSSION

The discussion positions the lattice as a design-space vocabulary while identifying substantial modeling, verification, evaluation, and empirical limitations. It also reports reproducible evidence that LangGraph’s default coordination mode admits observable L0 anomalies in third-party code.

Design-space interpretation: Deployed placements cluster at lower lattice levels; L3 guarantees appear only under restricted workloads, leaving unrestricted L3/L4 runtimes as open engineering territory.The lattice serves both to name current capabilities and to map the unfilled design space.
Model limitations: The operational model is proposed rather than derived from deployed runtimes, which use heterogeneous abstractions; validation across more runtimes remains future work.The model studies long-running concurrent operations under inference-bounded latency.
Verification limitations: TLC verification uses |A| = 2, |Cells| ≤2, and MaxOps ≤4; expanding to |A| = 3 and MaxOps = 6 exceeds 150 million states within ten minutes.The largest exhaustive run reached 9.3 million distinct states, so larger configurations require more compute, symmetry reduction, or symbolic methods.
Evaluation limitations: The evaluation covers two model providers, while the contention sweep is synthetic, single-model, and uses composed wall-clock figures rather than a concurrent deployed runtime.The real-LLM baseline includes 1,800 sessions across three workloads and runtimes on gpt-4o and Claude Sonnet 4.5; the sweep runs on gpt-4o-mini.
Empirical limitations: The reported 1%, 35%, and 100% anomaly rates are workload-engineered rather than production-observed, because prevalence requires instrumented, ethically cleared deployment traces.Production analysis must distinguish formalized concurrency anomalies from cognitive failures.
LangGraph evidence: 34 third-party repositories contain issues or pull requests mentioning LangGraph’s exact concurrent-update error strings, supporting reproducible occurrence of its default L0 anomaly class.The complete union contains 44 repositories from 50 and 56 matching issues/PRs; LangGraph’s default channel can fail-stop or permit overwriting behavior.

7 RELATED WORK

The paper adapts anomaly-based consistency hierarchies and refinement verification to long-running, shared-state multi-agent LLM runtimes. It positions this work relative to database isolation, distributed consistency, transactional memory, verified systems, workflow engines, and agent-memory substrates while explicitly limiting its theoretical claims.

Consistency models: Database isolation provides the closest conceptual ancestor, but this work applies anomaly-based stratification to long-running operations rather than conventional database workloads.The paper relates its hierarchy to snapshot-isolation serializability and production serializable systems such as PostgreSQL and CockroachDB.
Consistency models: Distributed consistency taxonomies similarly enumerate anomalies and stratify guarantees, but this lattice targets neural-inference latency rather than network propagation delay.The broader distributed-systems literature generally assumes discrete operations with summarizable signatures.
Concurrency control: Transactional memory and MVCC motivate the runtime designs, while the seconds-to-minutes cost of aborted inference favors pessimistic locking over optimistic abort-and-retry.The paper presents this recommendation as a special case of established software-transactional-memory contention-management policy space.
Verification: Mechanically verified distributed systems establish feasibility, but the paper’s Verus chain verifies finite-history detectors by refinement rather than certifying a running distributed store.Chapar is identified as the closest comparison to the L2 target, while IronFleet and Verdi demonstrate verified protocols at Paxos scale.
Workflow systems: Workflow engines operationally manage cascade and tool-effect reordering through saga-style compensation and deterministic replay; the paper presents corresponding models without claiming a new mechanism.Their replay requirement is described as a production instance of the paper’s deterministic-generation regime.
Agent systems: Agent-memory systems such as MemGPT and Letta make persistent shared mutable state central, yet provide no explicit consistency contract for concurrent memory edits.The paper treats them as candidate deployment substrates for its prevention contracts.

8 CONCLUSION

The paper presents a mechanically verified consistency hierarchy for multi-agent LLM systems, centered on mechanized realization rather than merely cataloging anomalies or defining a lattice. It formalizes four anomalies and verifies detectors, chain coherence, and runtime realizations across deployed and dependency-free runtimes.

Verified hierarchy: Four concurrency anomalies are formalized in TLA+ and exhibited through TLC counter-example traces at small finite parameters.A replication-aware extension is deferred for one further anomaly.
Verified hierarchy: The anomalies induce a Boolean lattice, from which the paper selects one operationally chosen maximal chain L0 ⊊ L1 ⊊ ··· ⊊ L4 among 4! = 24 possible chains.The lattice is L = ⟨2A,⊆⟩.
Mechanized realization: The substantive contribution is mechanized realization: Verus verifies detector soundness and completeness, while TLAPS checks coherence of the chain definitions.These verification results distinguish the contribution from the anomaly catalog and lattice themselves.
Runtime verification: Three deployed Rust runtimes are verified against stale-generation and refined to their state machines, while L2–L4 receive exec-mode-verified, dependency-free prevention twins.The refinements are grounded in concurrency primitives used by deployed frameworks.

APPENDIX

The appendix makes the verification totals auditable by reproducing per-file Verus accounting and correcting re-inclusion double counts. It reports 274 curated and 295 full distinct obligations, with every counted file verifying at 0 errors.

Verification accounting: 274 curated and 295 full distinct verified proof obligations are reported with 0 errors.The appendix reproduces the per-file accounting behind both totals.
Deduplication: 55 double-counted obligations are removed across four re-inclusion edges, with lib_l2_safety.rs subtracted twice for its two distinct parents.The deductions are −22, −6, −5, and −22.
Totals: The full total is 350 −55 = 295, while excluding four helper files removes 21 obligations and yields 329 −55 = 274.verus_count.sh reproduces the curated total, and verus_count.sh -full reproduces the full total.