Distributed Systems # TLA+ para Verificación Formal: Encontrando Bugs de Sistemas Distribuidos Antes de Escribir una Sola Línea de Código 2026-03-187 min lectura Lucio Durán Engineering Manager & AI Solutions Architect También disponible en: [English]() ## Fundamentos de TLA+ [TLA+]() (Temporal Logic of Actions) es el lenguaje de especificación formal de Leslie Lamport. No escribirs código en TLA+, escribirs un modelo matemático de tu sistema como una máquina de estados. Después se ejecuta el model checker TLC, que explora exhaustivamente cada estado posible que tu sistema puede alcanzar y verifica que tus invariantes se cumplan en todos ellos. El insight clave: los bugs de sistemas distribuidos no están en el código. Están en el *diseño*. Si tu protocolo está mal, ninguna cantidad de código cuidadoso o testing salvará. TLA+ encuentra bugs de diseño antes de que escribas una sola línea de código de implementación. Una especificación TLA+ mínima: ```tla ---- MODULE SimpleCounter ---- EXTENDS Integers VARIABLE count Init == count = 0 Increment == count < 10 /\ count' = count + 1 Next == Increment Spec == Init /\ [][Next]_count CountInvariant == count >= 0 /\ count <= 10 ==== ``` ## PlusCal: TLA+ para Humanos TLA+ crudo es notación matemática. PlusCal es un lenguaje de algoritmos que transpila a TLA+ y se lee más como pseudocódigo: ```tla ---- MODULE MutualExclusion ---- EXTENDS Integers, TLC CONSTANT NumProcesses (*--algorithm mutex variables lock = "free"; process proc \in 1..NumProcesses variables hasLock = FALSE; begin AcquireLock: await lock = "free"; lock := self; hasLock := TRUE; CriticalSection: skip; ReleaseLock: lock := "free"; hasLock := FALSE; goto AcquireLock; end process; end algorithm; *) MutualExclusion == \A p1, p2 \in 1..NumProcesses : (p1 /= p2) => ~(pc[p1] = "CriticalSection" /\ pc[p2] = "CriticalSection") ==== ``` Ejecutar TLC con ` NumProcesses = 3 ` y va a explorar cada posible interleaving de los tres procesos. Si dos procese es pueden estar alguna vez en la sección crítica simultáneamente, TLC produce un contraejemplo, una secuencia exacta de estados que lleva a la violación. ## El Ejemplo Real de Kafka La siguiente especificación encontró un bug real. Modela una versión simplificada del protocolo de rebalanceo de consumer groups de Kafka: ```tla ---- MODULE KafkaRebalance ---- EXTENDS Integers, Sequences, FiniteSets, TLC CONSTANTS Consumers, \* Conjunto de IDs de consumers Partitions, \* Conjunto de IDs de particiones MaxGenerations \* Límite de números de generación VARIABLES groupState, \* "empty" | "rebalancing" | "stable" generation, \* Número de generación actual members, \* Conjunto de consumers en el grupo leader, \* Consumer leader actual (o "none") assignment, \* Función: partición -> consumer (o "unassigned") consumerState, \* Función: consumer -> estado pendingJoins, \* Conjunto de consumers esperando unirse pendingSync \* Conjunto esperando respuesta de sync vars == <> TypeInvariant == /\ groupState \in {"empty", "rebalancing", "stable"} /\ generation \in 0..MaxGenerations /\ members \subseteq Consumers /\ leader \in Consumers \union {"none"} /\ \A p \in Partitions : assignment[p] \in Consumers \union {"unassigned"} /\ \A c \in Consumers : consumerState[c] \in {"idle", "joining", "active", "failed"} Init == /\ groupState = "empty" /\ generation = 0 /\ members = {} /\ leader = "none" /\ assignment = [p \in Partitions |-> "unassigned"] /\ consumerState = [c \in Consumers |-> "idle"] /\ pendingJoins = {} /\ pendingSync = {} \* Un consumer falla (crashea) ConsumerFail(c) == /\ consumerState[c] \in {"joining", "active"} /\ consumerState' = [consumerState EXCEPT ![c] = "failed"] /\ members' = members \ {c} \* EL BUG ESTABA ACÁ: assignment no se limpiaba inmediatamente \* Original (buggy): UNCHANGED <> \* Fix: limpiar assignments del consumer fallido /\ assignment' = [p \in Partitions |-> IF assignment[p] = c THEN "unassigned" ELSE assignment[p]] /\ IF leader = c THEN leader' = IF members' /= {} THEN CHOOSE m \in members' : TRUE ELSE "none" ELSE UNCHANGED leader /\ UNCHANGED <> \* SAFETY: Ninguna partición asignada a un consumer fallido NoFailedAssignment == \A p \in Partitions : assignment[p] /= "unassigned" => consumerState[assignment[p]] /= "failed" \* SAFETY: Todos los consumers asignados son miembros del grupo AssignedAreMembers == \A p \in Partitions : assignment[p] /= "unassigned" => assignment[p] \in members ==== ``` ## El Bug que TLC Encontró Al ejecutar esto con el ` UNCHANGED <> ` original en la acción ` ConsumerFail `, TLC encontró una violación de ` NoFailedAssignment ` en 6 estados: ``` Error: Invariant NoFailedAssignment is violated. Error trace: 1: groupState = "empty", generation = 0, members = {} 2: JoinGroup("c1") consumerState["c1"] = "joining" 3: JoinGroup("c2") consumerState["c2"] = "joining" 4: TriggerRebalance generation = 1, members = {"c1", "c2"}, leader = "c1" 5: LeaderAssign assignment = [1 |-> "c1", 2 |-> "c2", 3 |-> "c1", 4 |-> "c2"] 6: ConsumerFail("c2") consumerState["c2"] = "failed", members = {"c1"} assignment = [1 |-> "c1", 2 |-> "c2", 3 |-> "c1", 4 |-> "c2"] ^^^^^^^^^^^^^^^^^^^^^^^^ c2 está failed pero sigue asignado a particiones 2 y 4! ``` El fix es obvio una vez que lo ves: cuando un consumer falla, limpiar inmediatamente sus asignaciones de particiones. Pero en la implementación real, la limpieza de assignments pasaba durante el *próximo* rebalanceo, no al momento de detección de falla. Esto significaba que había una ventana donde un nuevo consumer podía unirse, desencadenar un rebalanceo, y el algoritmo de asignación del leader podía ver la asignación vieja y tomar decisiones conflictivas. Este tipo de ventana puede existir en sistemas de producción durante meses. TLC la encuentra en 0.3 segundos. ## Corriendo el Model Checker ```bash # Crear archivo de config (KafkaRebalance.cfg) cat > KafkaRebalance.cfg << 'EOF' CONSTANTS Consumers = {"c1", "c2", "c3"} Partitions = {1, 2, 3, 4} MaxGenerations = 3 INIT Init NEXT Next INVARIANTS TypeInvariant NoFailedAssignment AssignedAreMembers EOF # Correr TLC java -jar tla2tools.jar -config KafkaRebalance.cfg KafkaRebalance.tla # Output: # Model checking completed. No errors found. # 847,293 states generated, 234,521 distinct states found. # Finished in 00:00:04 (4 seconds) ``` 847,293 estados. Cada posible interleaving de joins, fallas, rebalanceos y asignaciones de leader con 3 consumers, 4 particiones y hasta 3 generaciones. Explorado exhaustivamente en 4 segundos. Sin randomness, sin "ojalá peguemos el bug", certeza matemática de que los invariantes se cumplen. ## Propiedades Temporales: Liveness Las propiedades de safety ("cosas malas nunca pasan") enganchan muchos bugs, pero las propiedades de liveness ("cosas buenas eventualmente pasan") enganchan una clase diferente: ```tla \* LIVENESS: Cada partición es eventualmente asignada a un consumer activo EventuallyAssigned == \A p \in Partitions : <>(assignment[p] /= "unassigned" /\ consumerState[assignment[p]] = "active") \* LIVENESS: El grupo eventualmente se estabiliza después de un rebalanceo EventuallyStable == groupState = "rebalancing" ~> groupState = "stable" ``` El operador ` <> ` significa "eventualmente". El operador ` ~> ` significa "lleva a". Estos requieren que TLC chequee propiedades temporales, lo que es más lento pero engancha bugs de liveness como bloqueo permanente o starvation. ## Patrones Prácticos Reutilizables ### Modelando Particiones de Red ```tla VARIABLE connected NetworkPartition(n1, n2) == /\ connected' = [connected EXCEPT ![{n1, n2}] = FALSE] /\ UNCHANGED <> SendMessage(from, to, msg) == /\ connected[{from, to}] /\ \* ... resto de la lógica de envío ``` ### Modelando Pérdida y Reordenamiento de Mensajes ```tla VARIABLE messages \* Conjunto de mensajes en vuelo (desordenado por diseño) Send(msg) == /\ messages' = messages \union {msg} Receive(msg) == /\ msg \in messages /\ messages' = messages \ {msg} \* Los mensajes también pueden perderse LoseMessage(msg) == /\ msg \in messages /\ messages' = messages \ {msg} /\ UNCHANGED <> ``` ## Cuándo No Usar TLA+ TLA+ es overkill para la mayoría del software. Utilizarlo cuando: 1. **La correctitud es crítica y el testing es insuficiente.** Protocolos de consenso distribuido, estructuras de datos lock-free, niveles de aislamiento de transacciones. 2. **El espacio de interacción es muy grande para testing.** 5 nodos, cada uno con 4 estados, 3 tipos de mensajes, falla en cualquier punto, son billones de interleavings. 3. **El costo de un bug es alto.** Corrupción de datos, pérdida financiera, sistemas safety-critical. No lo uses para: - Aplicaciones CRUD - Servicios request-response simples - Cualquier cosa donde la parte difícil es la UI o lógica de negocio y no el protocolo de concurrencia La curva de aprendizaje es real, unas 3 semanas de estudio dedicado para ir de cero a productivo. Pero dado el historial de TLC encontrando bugs en protocolos que parecían obviamente correctos, modelar cada protocolo distribuido no trivial antes de implementar es una inversión sólida. Una spec usualmente lleva 2-3 días. Encontrar y arreglar un bug de concurrencia en producción lleva 2-3 semanas. La matemática es accesible. ## Preguntas frecuentes ### ¿Qué es TLA+ y por qué usarlo para sistemas distribuidos? TLA+ es un lenguaje de especificación formal basado en lógica temporal de acciones. Modelás tu sistema como una máquina de estados, se define invariantes, y se ejecuta el model checker TLC para explorar exhaustivamente todos los estados posibles. Encuentra bugs que el testing no puede, como condiciones de carrera que solo se manifiestan con un ordenamiento específico de mensajes entre 5 nodos. ### ¿Es TLA+ práctico para equipos de ingeniería reales? Sí. Amazon usa TLA+ extensivamente, encontraron bugs críticos en DynamoDB, S3 y EBS usando verificación formal. La curva de aprendizaje es empinada (2-3 semanas para ser productivo), pero para sistemas donde la correctitud es crítica, la inversión rinde dramáticamente. ### ¿En qué se diferencia TLA+ del property-based testing? Property-based testing genera inputs random y chequea propiedades contra tu código real. TLA+ chequea propiedades contra un modelo matemático de tu sistema explorando exhaustivamente todos los estados posibles. Property-based testing puede perder bugs escondidos en estados no explorados; TLA+ los encuentra todos. ## Tips 1. **Tip:** Comenzar con ` PlusCal ` en vez de TLA+ crudo. PlusCal es un lenguaje de algoritmos que transpila a TLA+ y se lee como pseudocódigo. Una vez que TLC encuentra un bug, se va a necesitar leer la traducción TLA+ para entender el error trace, pero para escribir specs, PlusCal te corta la curva de aprendizaje a la mitad. 2. **Tip:** Mantener tu espacio de estados pequeño usando ` CONSTANTS ` con valores mínimos, 2 nodos, 3 mensajes máximo, 2 epochs. TLC explora cada estado alcanzable; pasar de 2 nodos a 3 puede aumentar el espacio de estados 100x. Solo subí los valores después de que tu spec pase con constantes pequeñas. 3. **Tip:** Siempre agregar un ` TypeInvariant ` que restrinja cada variable a su dominio esperado. Sin él, un typo en tu spec (como asignar un string donde esperás un integer) crea millones de estados basura y TLC corre por horas antes de hacer OOM. El type invariant lo engancha en segundos. 4. **Tip:** Ejecutar TLC con el flag ` -deadlock ` deshabilitado cuando recién empezás a modelar. Muchos diseños válidos de sistemas distribuidos tienen estados terminales (como todos los nodos apagándose) que TLC marca como deadlocks por defecto. - tla-plus - verificación-formal - sistemas-distribuidos - model-checking - lógica-temporal - kafka - consenso [Volver al Blog]()