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.
En 30 segundos
- Los LLMs pasan validación sintáctica de TLA+ cercana al 100%, pero solo el 46% logra conformidad real con el sistema modelado.
- El benchmark SysMoBench evalúa cuatro fases: sintaxis, runtime, conformidad de trazas e invariantes, sobre once sistemas reales como Etcd Raft y ZooKeeper.
- Dos patrones de fallo sistemáticos: los modelos entran en estados que el sistema real nunca alcanza, o no alcanzan estados que siempre suceden.
- El problema de raíz es que los LLMs recitan el protocolo teórico (el paper de Raft) en lugar de modelar cómo la implementación concreta se comporta.
- Un agente “traductor” código-a-TLA+ supera al modelo base en sistemas complejos; la adherencia al código fuente reduce las alucinaciones.
¿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.