Detección y Prevención Verificadas de Anomalías de Concurrencia en Sistemas Multiagente de Grandes Modelos de Lenguaje

Resumen

Los sistemas multiagente de LLM comparten estado a través de almacenes de memoria, índices vectoriales y registros de herramientas. Modelamos dicha compartición como operaciones de lectura-generación-escritura de larga duración bajo semántica de generación determinista —el régimen que los motores de ejecución durable imponen mediante repetición determinista— y formalizamos cuatro anomalías de concurrencia en TLA+: stale-generation, phantom-tool, causal-cascade y tool-effect reordering, análogos estructurales de anomalías clásicas de aislamiento, cada una con un contraejemplo en TLC. El retículo de exclusión sobre estas anomalías es trivial; la contribución es la realizabilidad verificada mecánicamente y la separación estricta de una cadena máxima dentro de él, \(L_0 \subsetneq \cdots \subsetneq L_4\), que constituye, hasta donde sabemos, la primera jerarquía de consistencia verificada por ordenador para tales entornos de ejecución. Un desarrollo de 274 obligaciones de Verus (cero suposiciones, cero admisiones; base de confianza: dos axiomas estructurales y una correspondencia de exclusión mutua) demuestra que los detectores son sólidos y completos respecto a las especificaciones, y que cada entorno de ejecución cumple su conjunto de evitación. Tres entornos de ejecución en Rust en producción materializan \(L_0\)–\(L_1\) (bloqueo pesimista, aislamiento de instantánea serializable, SI predeterminado), cada uno verificado frente a stale-generation y refinado hasta su máquina de estados; \(L_2\)–\(L_4\) se verifican en modo de ejecución con gemelos de prevención libres de dependencias (A3, A6, A2: 0/1000 frente a 1000/1000), y \(L_2\) se ejecuta en vivo en tres familias de modelos (A3 prevenido en las 120 sesiones retraídas). Reproducimos una actualización perdida silenciosa en deer-flow de ByteDance, formalizando su corrección como un refinamiento verificado de \(L_0\) a \(L_1\), y exhibimos reordenamiento de efecto de herramienta en ToolNode de LangGraph sobre salida sin modificar, eliminado mediante un secuenciador de orden de confirmación de nivel \(L_3\). El detector verificado, los refinamientos y los artefactos de realizabilidad constituyen la contribución; los fenómenos y el retículo son clásicos.

English

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.