TLA+ para Verificación Formal: Encontrando Bugs de Sistemas Distribuidos Antes de Escribir una Sola Línea de Código

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:

---- 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:

---- 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:

---- 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 == <<groupState, generation, members, leader, assignment,
 consumerState, pendingJoins, pendingSync>>

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 <<assignment>>
 \* 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 <<groupState, generation, pendingJoins, pendingSync>>

\* 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 <<assignment>> original en la acción ConsumerFail, TLC encontró una violación de NoFailedAssignment en 6 estados:

Error: Invariant NoFailedAssignment is violated.

Error trace:
1: <Init>
 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

# 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:

\* 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

VARIABLE connected

NetworkPartition(n1, n2) ==
 /\ connected' = [connected EXCEPT ![{n1, n2}] = FALSE]
 /\ UNCHANGED <<otherVars>>

SendMessage(from, to, msg) ==
 /\ connected[{from, to}]
 /\ \* ... resto de la lógica de envío

Modelando Pérdida y Reordenamiento de Mensajes

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 <<otherVars>>

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.