No puedes hacer pruebas unitarias de un protocolo distribuido. Una prueba unitaria ejecuta un proceso en una máquina en un orden determinado. Tu protocolo ejecuta diez procesos en cinco máquinas en un orden que no controlas. La brecha entre esas dos realidades es donde viven tus errores.

El model checking cierra esa brecha. Explora todas las intercalaciones posibles de todos los estados que tu protocolo puede alcanzar. Si hay una forma de que dos réplicas discrepen, una forma de que una elección de líder se bloquee, o una forma de que surja un escenario de cerebro dividido, el model checker lo encontrará. Y lo encontrará antes de que hayas escrito el primer controlador de RPC.

Por qué los errores distribuidos sobreviven a las pruebas tradicionales

La explosión de estados es el problema. Tres nodos intercambiando mensajes pueden producir miles de millones de caminos de ejecución. Las pruebas de integración escritas a mano cubren quizás una docena de ellos, normalmente el camino feliz y un par de modos de fallo obvios. ¿El error en el que el nodo A falla exactamente entre enviar un prepare y un ack? Buena suerte reproduciéndolo en CI.

La verificación formal suena a ejercicio académico, pero el model checking es diferente. No demuestras que el protocolo sea correcto para siempre. Describes el protocolo en un lenguaje de especificación, defines las propiedades que te importan, y dejas que una herramienta busque exhaustivamente en el espacio de estados hasta cierto límite. Cuando encuentra una violación, te entrega un rastro mínimo. Obtienes una receta paso a paso para reproducir el error. Nada de heisenbugs. Nada de “funciona en mi máquina”.

La herramienta más práctica para esto es TLA+, desarrollada por Leslie Lamport. Parece matemáticas porque lo es. Pero las matemáticas son más simples de lo que esperas, y la recompensa es encontrar errores que de otro modo surgirían a las 2 AM en producción.

Qué hace realmente el model checking

Un model checker toma tres entradas: una descripción de tu sistema, una descripción de su entorno, y las propiedades que quieres que se cumplan. La descripción del sistema captura la lógica de tu protocolo. La descripción del entorno captura todo lo que no controlas: retrasos de red, pérdida de mensajes, fallos de nodos, desviación de relojes. Las propiedades suelen ser invariantes (“el registro confirmado nunca se sobrescribe”) o condiciones de vivacidad (“toda solicitud eventualmente recibe una respuesta”).

El model checker genera entonces cada estado alcanzable y cada transición válida entre ellos. Lo hace de forma exhaustiva para espacios de estados finitos, o con exploración acotada para los infinitos. Si se viola una invariante, se detiene y reporta el camino más corto al fallo.

Esto es fuerza bruta, no magia. El model checker no entiende tu intención. Simplemente lo prueba todo. Ese es exactamente el punto. Tus pruebas de integración están sesgadas por tus suposiciones. El model checker no tiene suposiciones.

Especificando un protocolo de consenso simple en TLA+

Veamos un ejemplo mínimo: un protocolo de consenso de decreto único donde un líder propone un valor y un quórum de aceptadores debe aceptarlo antes de que el valor sea elegido. Esta es la idea central detrás de Paxos, Raft y cualquier otro algoritmo de consenso que hayas escuchado.

Aquí está la especificación TLA+ del sistema:

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

Esta especificación dice: inicialmente nada está elegido. Una acción de proponer puede establecer chosen a un único valor, pero solo si aún no se ha elegido nada. La invariante ChosenUniqueness establece que como máximo un valor puede ser elegido en cualquier momento.

El model checker de TLA+, TLC, verificará que ningún rastro de ejecución viole ChosenUniqueness. Si introduces un error donde dos líderes pueden proponer simultáneamente sin verificar valores previos, TLC encuentra el contraejemplo en milisegundos.

Agregando las partes desordenadas: fallos y pérdida de mensajes

La especificación anterior es demasiado limpia. Los sistemas distribuidos reales no son limpios. Los mensajes se pierden. Los nodos se reinician. Las particiones de red aislan grupos de nodos entre sí. El modelo solo se vuelve útil cuando modelas estos fallos.

Aquí hay un fragmento más realista que modela el paso de mensajes con pérdida potencial:

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop es la adición importante. Modela la pérdida de mensajes sin cambiar el estado del aceptador. TLC explorará trazas donde cualquier mensaje es entregado, descartado o retrasado indefinidamente. Cuando agregas un fallo y recuperación del líder, el espacio de estados crece, pero TLC sigue explorándolo sistemáticamente.

Esta es la parte que me confundió cuando empecé con TLA+. Quería modelar solo la lógica del protocolo. Pero los errores no estaban en la lógica. Estaban en la interacción entre la lógica y los modos de fallo que no había considerado. Tienes que modelar ambos.

La compensación: explosión del espacio de estados y abstracción

El model checking no es gratis. El número de estados crece exponencialmente con el número de procesos y el tamaño de tus cargas útiles de mensajes. Una especificación con cinco valores y tres aceptadores podría generar millones de estados. Agrega un cuarto aceptador y estás en miles de millones. Ejecútalo en tu laptop y se quedará sin memoria antes de terminar.

La solución es la abstracción. No modelas tus valores reales de 64 bytes. Modelas dos valores: V1 y V2. Si el protocolo se comporta correctamente para dos valores, los valores específicos no importan. No modelas un registro de 10,000 entradas. Modelas un registro de profundidad 2. Si la seguridad se cumple para profundidad 2, casi siempre se cumple para profundidad arbitraria. Esto se llama model checking de modelo pequeño, y es la práctica estándar en el campo.

La habilidad clave es aprender qué detalles importan y cuáles no. Los contenidos de los mensajes usualmente no importan para las propiedades de seguridad. El orden de los mensajes casi siempre importa. Las identidades de los nodos podrían no importar, pero el número de nodos en cada rol sí.

Si el espacio de estados sigue siendo demasiado grande, tienes otras opciones. Puedes usar reducción por simetría para tratar nodos idénticos como intercambiables. Puedes acotar la profundidad de la búsqueda. O puedes cambiar a un model checker simbólico como Apalache, que usa solucionadores SMT para razonar sobre estados sin enumerarlos todos.

De la especificación a la implementación: manteniéndolas sincronizadas

Una especificación verificada no vale nada si tu implementación diverge de ella. La especificación es el plano. El código es el edificio. No hay un puente automatizado entre los dos, y esa brecha es donde los errores se cuelan de nuevo.

El enfoque práctico es tratar la especificación TLA+ como un documento de diseño que resulta ser ejecutable. Revísalo junto con el código durante las pull requests. Cuando la implementación maneja un caso límite, pregúntate si la especificación también lo maneja. Cuando encuentres un error en producción, verifica si la especificación lo habría detectado. Si no, actualiza la especificación.

Algunos equipos van más allá y generan casos de prueba a partir de los contraejemplos que produce TLC. Un rastro de TLC mostrando cómo dos réplicas divergen se convierte en un escenario de prueba de integración. Este es trabajo manual, pero conecta el modelo formal a tu suite de pruebas.

En Sentry, usamos este enfoque para validar un protocolo de limitación de tasa distribuido. La especificación detectó un problema de vivacidad donde un nodo en recuperación podía sufrir inanición en un escenario de partición específico. Nuestras pruebas de integración nunca lo habían disparado porque siempre sanaban las particiones limpiamente. El model checker no se preocupaba por lo limpio. Probó el caso desordenado, encontró el error y nos ahorró un incidente muy confuso.

Cómo empezar: tu primera verificación de modelos

Si quieres probar esto, empieza con el TLA+ Toolbox. Es un IDE gratuito para escribir y verificar especificaciones. Trabaja con los ejemplos de Paxos y Raft que vienen incluidos. Son más complejos que el fragmento de consenso de arriba, pero muestran cómo se modelan protocolos reales.

Para tu primera especificación, elige algo pequeño de tu propio sistema. Un protocolo de elección de líder. Un esquema de invalidación de caché distribuida. Una variante de confirmación en dos fases. Escribe las invariantes que crees que se cumplen. Luego deja que TLC te diga si tienes razón. Normalmente dice que no, y normalmente lo dice dentro de la primera hora.

El model checking no encontrará todos los errores. No ayudará con el rendimiento, no detectará errores de serialización, y no verificará que tu implementación coincida con tu especificación. Lo que sí hace es encontrar los errores profundos de protocolo que las pruebas de integración omiten, y los encuentra en tiempo de diseño, cuando las correcciones no cuestan nada.

Esa es la corrección de errores más barata en sistemas distribuidos. No un depurador mejor. No más monitoreo. Atrapar el error antes de que el código exista siquiera.