LLMs y TLA+: el 54% falla en modelar sistemas reales

Los LLMs generan especificaciones TLA+ con sintaxis perfecta, pero solo el 46% alcanzan conformidad real con el comportamiento del sistema, y apenas el 41% satisfacen los invariantes críticos. Eso es el hallazgo central de SysMoBench, un benchmark publicado en 2026 que evalúa a los modelos en once sistemas distribuidos reales.

¿Qué es TLA+ y por qué importa para sistemas distribuidos?

TLA+ es un lenguaje de especificación formal creado por Leslie Lamport que permite describir el comportamiento de un sistema con precisión matemática y verificar propiedades críticas como seguridad y vivacidad. No es un lenguaje de programación: no se ejecuta en producción. Se usa para pensar el sistema antes de construirlo, o para verificar que lo que ya existe hace lo que creés que hace.

Si alguna vez te preguntaste cómo Amazon Web Services garantiza que DynamoDB no pierda datos bajo condiciones de partición, la respuesta incluye TLA+. Los ingenieros de AWS lo usan para verificar algoritmos de consenso distribuido antes de escribir una sola línea de código de producción. Lo mismo con Etcd, el almacén de configuración que corre debajo de Kubernetes, o con ZooKeeper, que coordina clusters de Hadoop y Kafka.

La diferencia crítica que hay que entender es esta: especificar un sistema no es lo mismo que describir el protocolo teórico en el que se inspiró. Etcd implementa Raft, sí. Pero la forma concreta en que Etcd aplica Raft tiene detalles, decisiones de diseño y comportamientos específicos que el paper original de Raft no captura. Ahí está el problema.

El desafío: LLMs modelar sistemas TLA+ sin cometer errores de fondo

Podés pedirle a cualquier LLM moderno que genere una especificación TLA+ de Etcd Raft y vas a obtener algo que el parser de TLA+ va a aceptar sin chistar. Sintaxis perfecta. Variables declaradas, operadores bien formados, invariantes que parecen correctos.

Y ahí está la trampa.

Según la investigación publicada en SIGOPS en 2026, cuando corrés esas especificaciones en el model checker TLC y las comparás contra el comportamiento real del sistema, los números se caen. El 46% de las specs generadas logran conformidad de trazas con el sistema real. El 41% satisfacen los invariantes definidos. El resto genera specs que se ven bien pero modelan un sistema que no existe.

Esto no es un problema menor de afinamiento. Es un problema estructural: los modelos aprenden a reproducir la forma de TLA+ pero no aprenden a razonar sobre qué estado puede o no puede alcanzar un sistema real bajo condiciones de falla. Lo explicamos a fondo en cómo construir sistemas LLM robustos.

SysMoBench: cómo se evalúan realmente los LLMs en verificación formal

El benchmark que hace posible esta medición se llama SysMoBench (o Specula en algunas referencias del paper). Evalúa las especificaciones generadas por LLMs en cuatro fases progresivas:

• Fase 1 — Sintaxis: ¿La spec es parseable por el toolchain de TLA+?
• Fase 2 — Runtime: ¿El model checker TLC puede ejecutarla sin errores internos?
• Fase 3 — Conformidad de trazas: ¿Las secuencias de estados que genera la spec corresponden a lo que el sistema real produce?
• Fase 4 — Invariantes: ¿Se satisfacen las propiedades críticas de seguridad y vivacidad definidas para el sistema?

Los once sistemas evaluados incluyen Etcd Raft, ZooKeeper, Multi-Paxos y otros protocolos de consenso y coordinación con implementaciones reales en producción. El dataset no fue construido con ejemplos de tutorial: son los sistemas que corren en infraestructura crítica hoy.

Los resultados por sistema varían bastante. En sistemas simples como un spinlock, los LLMs llegan a tasas de conformidad razonables. En Etcd Raft y ZooKeeper, los números caen consistentemente. La complejidad del sistema es el factor más predictivo de fracaso (lo cual tiene sentido, pero igual hay que medirlo para creerlo).

Dos patrones sistemáticos de fallo en especificaciones

El análisis del paper identifica dos patrones recurrentes que explican la mayoría de los errores. No son bugs aleatorios: son errores conceptuales sistemáticos.

Patrón 1: La spec entra en estados que el sistema real nunca alcanza. El model checker explora un espacio de estados que incluye configuraciones imposibles en la implementación real. La spec es “demasiado permisiva”: permite comportamientos que el código real prohibe, ya sea por precondiciones implícitas, por cómo están inicializadas las variables, o por invariantes que el sistema mantiene pero que el LLM no capturó.

Patrón 2: La spec no alcanza estados que el sistema real siempre alcanza. El caso ZooKeeper es ilustrativo: el sistema real sobrescribe los votos cuando llega una nueva elección, pero la spec generada los acumula como unión de conjuntos. El resultado es un modelo que se queda atascado antes de llegar a estados de liderazgo que en producción son rutinarios.

¿Por qué ocurren ambos patrones? Porque el LLM no está mirando el código. Está mirando lo que aprendió de papers, documentación y discusiones de Stack Overflow. Complementá con optimizar costos de modelos abiertos.

¿Por qué los LLMs recitan papers en lugar de modelar código real?

Acá está el problema de fondo: cuando le pedís a un LLM que modele Etcd Raft en TLA+, el modelo genera la especificación del algoritmo Raft tal como aparece en el paper de Ongaro y Ousterhout de 2014. No modela cómo Etcd implementa Raft en Go, con todas sus decisiones de diseño, sus timeouts particulares, su manejo de configuración dinámica del cluster, sus optimizaciones de snapshot.

La diferencia es enorme. El paper de Raft describe un protocolo abstracto. Etcd es una implementación concreta con años de decisiones de ingeniería encima. Modelar uno en lugar del otro te da una spec que pasa todos los tests unitarios del protocolo teórico y falla en los invariantes que importan en producción.

Esto no es un problema que se resuelva con más parámetros o más entrenamiento en TLA+. El modelo tendría que ver el código fuente real, entender sus invariantes implícitos, y traducir eso a lógica temporal. Es un problema diferente al de “escribir código que compila”.

Estrategias que funcionan mejor: agentes traductores vs. modeladores

La investigación también prueba variantes de agentes. El hallazgo más útil para quien quiera usar LLMs en verificación formal hoy es este: un agente “traductor” (que trabaja código-a-TLA+ línea a línea, anclado al código fuente) supera al agente “modelador” (que genera la spec de memoria) en sistemas complejos.

La diferencia conceptual: el traductor no tiene libertad para inventar. Va leyendo el código real y produciendo la abstracción TLA+ correspondiente. Cuando el código dice “si el término del mensaje es mayor al término local, actualizá el término y convertite en follower”, el agente traduce exactamente eso. No recita la versión del paper.

Esto reduce las alucinaciones porque el modelo está anclado a una fuente de verdad concreta en lugar de depender de lo que recuerda de su entrenamiento. La precisión mejora, especialmente en los invariantes (el aspecto más difícil).

Enfoque	Conformidad de trazas	Satisfacción de invariantes	Mejor para
LLM base (sin contexto)	~46%	~41%	Sistemas simples
LLM con spec de referencia	Mejora marginal	Mejora marginal	Sistemas documentados
Agente traductor (código-a-TLA+)	Mejora significativa	Mejor resultado actual	Sistemas complejos con código disponible
Verificación manual post-LLM	Depende del revisor	Alta si se hace bien	Sistemas críticos en producción

Lo que no está disponible todavía es un pipeline completamente automatizado que funcione de punta a punta sin revisión humana en sistemas complejos. Para spinlocks y protocolos simples, zafa. Para Raft o Paxos, todavía necesitás a alguien que entienda el sistema. Te puede servir nuestra cobertura de nuevos modelos de facturación por tokens.

Implicaciones prácticas: cuándo confiar en LLMs para verificación formal

Si estás en un equipo que usa TLA+ para verificar sistemas distribuidos, la pregunta práctica es: ¿en qué parte del flujo meto un LLM y en qué parte no?

Hoy, los LLMs son útiles para generar un borrador inicial que un ingeniero con experiencia en TLA+ pueda revisar y corregir. Eso solo ya ahorra tiempo. La alternativa es escribir la spec desde cero, que lleva días. Tener un punto de partida razonablemente bien formado que necesita correcciones específicas es mejor que nada.

Lo que no vas a querer hacer es tomar la spec generada y correrla en TLC sin revisión, asumir que si pasa la validación sintáctica la spec es correcta, y menos aún usarla para certificar que tu sistema es seguro. Eso sería usar el 46% como si fuera el 100%.

El roadmap que sugieren los investigadores incluye hibridación: LLMs que generan hipótesis de especificación + métodos formales que las verifican automáticamente + loops de refinamiento guiados por los contraejemplos del model checker. No es ciencia ficción, pero tampoco está en producción todavía en 2026.

Para equipos que necesitan verificación formal de sistemas críticos y están evaluando proveedores de infraestructura para sus entornos de desarrollo y testing, la infraestructura donde corren estos pipelines importa tanto como el modelo que usan. donweb.com tiene opciones de VPS para este tipo de workloads en Argentina.

Errores comunes al usar LLMs para generar TLA+

Error 1: Confundir validación sintáctica con corrección. El parser de TLA+ no sabe si tu spec modela el sistema real. Solo sabe si la escribiste bien. Un artículo que parece gramaticalmente correcto puede decir cualquier barbaridad. Lo mismo pasa con las specs.

Error 2: Pedirle al LLM que modele “Raft” en lugar de “Etcd”. Son cosas distintas. Si querés verificar propiedades de Etcd, la spec tiene que reflejar cómo Etcd implementa Raft, no el algoritmo abstracto. El prompt importa: mencioná el sistema concreto, pasale fragmentos del código fuente, pedile que se ancle a la implementación. Relacionado: limitaciones en herramientas IA modernas.

Error 3: No definir los invariantes antes de pedir la spec. Si no tenés claro qué propiedades querés verificar, el LLM va a inventar invariantes que suenan razonables pero que capturan propiedades triviales o incorrectas. Los invariantes son la parte más valiosa de una spec formal y no pueden quedar implícitos en el prompt.

Preguntas Frecuentes

¿Pueden los LLMs modelar correctamente sistemas reales en TLA+?

Depende del sistema y de cómo se usa el LLM. Para sistemas simples como un spinlock, los modelos actuales logran tasas de conformidad razonables. Para sistemas complejos como Etcd Raft o ZooKeeper, el 46% de conformidad de trazas y el 41% de satisfacción de invariantes indican que la mitad de las specs generadas modelan un sistema incorrecto. No es una solución lista para usar sin revisión humana.

¿Qué limitaciones tienen los LLMs para especificaciones formales?

El problema central es que los modelos generan specs basadas en lo que aprendieron de papers y documentación, no en el código real de la implementación. Esto produce especificaciones del protocolo teórico en lugar del sistema concreto. Dos patrones de fallo recurrentes: la spec permite estados que el sistema real nunca alcanza, o no alcanza estados que siempre ocurren en producción.

¿Cómo se valida si una especificación TLA+ de un LLM es correcta?

Con el model checker TLC, comparando las trazas de estado que genera la spec contra trazas reales del sistema. SysMoBench formaliza este proceso en cuatro fases: validación sintáctica, ejecución en runtime, conformidad de trazas y satisfacción de invariantes. Pasar la fase 1 (sintaxis) no implica pasar las siguientes tres.

¿Qué diferencia hay entre sintaxis correcta y conformidad real en TLA+?

Una spec sintácticamente correcta es una que el parser de TLA+ acepta sin errores. Una spec con conformidad real es una que modela el comportamiento observable del sistema: las mismas secuencias de estados, las mismas transiciones, los mismos invariantes. Los LLMs actuales alcanzan casi el 100% en sintaxis y cerca del 46% en conformidad. La distancia entre esos números es el problema.

¿Cuál es el mejor enfoque para LLMs generando TLA+ preciso?

El agente traductor, que trabaja línea a línea desde el código fuente hacia TLA+, supera al modelo base en sistemas complejos. La clave es anclar el modelo al código real, no dejarlo generar desde memoria. Combinado con revisión humana de los invariantes y loops de refinamiento guiados por contraejemplos del model checker, los resultados mejoran. No existe todavía un pipeline completamente automatizado que funcione sin supervisión en sistemas críticos.

Conclusión

Lo que muestra esta investigación publicada en 2026 es que hay una brecha real entre lo que los LLMs parecen capaces de hacer en verificación formal y lo que efectivamente hacen. Generar TLA+ con sintaxis correcta es un problema resuelto. Modelar el comportamiento de un sistema distribuido real con la precisión suficiente para que el model checker encuentre bugs verdaderos, ese es el problema abierto.

Para equipos que usan TLA+ hoy, la recomendación práctica es clara: los LLMs son útiles como generadores de borradores que aceleran el trabajo inicial, no como sustitutos del razonamiento formal. El agente traductor anclado al código fuente es el enfoque más prometedor en este momento. Y los invariantes siempre los definís vos, no el modelo.

El horizonte interesante está en la hibridación: LLMs que formulan hipótesis + model checkers que las falsifican + agentes que refinan. Eso todavía no existe como producto, pero es hacia donde apunta la investigación.

Fuentes

• SIGOPS 2026 — Can LLMs Model Real-World Systems in TLA+?
• arXiv 2509.23130 — SysMoBench: Benchmarking LLMs on Formal System Modeling
• arXiv 2512.09758 — LLMs for Formal Specification Generation
• GitHub: yuzhoumao/llm-formal — Código y dataset del benchmark
• arXiv 2604.01851 — Agent-based Translation for TLA+ Specification