Você não pode fazer unit test de um protocol distribuído. Um unit test executa um processo em uma máquina em uma ordem. Seu protocol executa dez processos em cinco máquinas em uma ordem que você não controla. A lacuna entre essas duas realidades é onde seus bugs vivem.

O model checking fecha essa lacuna. Ele explora todos os possíveis entrelaçamentos de todos os possíveis estados que seu protocol pode alcançar. Se há uma forma de duas replicas discordarem, uma forma de uma leader election entrar em deadlock, ou uma forma de um cenário de split-brain surgir, um model checker encontrará. E encontrará antes que você tenha escrito o primeiro RPC handler.

Por que bugs distribuídos sobrevivem aos testes tradicionais

A explosão de estados é o problema. Três nodes trocando mensagens podem produzir bilhões de caminhos de execução. Os integration tests escritos à mão cobrem talvez uma dúzia deles, geralmente o happy path e alguns failure modes óbvios. O bug em que o node A falha exatamente entre enviar um prepare e um ack? Boa sorte em acertar isso no CI.

A verificação formal soa como um exercício acadêmico, mas o model checking é diferente. Você não prova que o protocol está correto para todo o sempre. Você descreve o protocol em uma linguagem de especificação, define as propriedades que se importa e deixa uma ferramenta buscar exaustivamente no espaço de estados até algum limite. Quando encontra uma violação, entrega a você uma trace mínima. Você recebe uma receita passo a passo para reproduzir o bug. Nada de heisenbugs. Nada de “funciona na minha máquina”.

A ferramenta mais prática para isso é o TLA+, desenvolvido por Leslie Lamport. Parece matemática porque é matemática. Mas a matemática é mais simples do que você espera, e o retorno é encontrar bugs que, de outra forma, surgiriam às 2h da manhã em produção.

O que o model checking realmente faz

Um model checker recebe três entradas: uma descrição do seu sistema, uma descrição do seu ambiente e as propriedades que você quer que se mantenham. A descrição do sistema captura a lógica do seu protocol. A descrição do ambiente captura tudo o que você não controla: delays de rede, perda de mensagens, falhas de nodes, skew de relógio. As propriedades costumam ser invariantes (“o log committed nunca é sobrescrito”) ou condições de liveness (“toda request eventualmente recebe uma response”).

O checker então gera cada estado alcançável e cada transição válida entre eles. Faz isso exaustivamente para espaços de estados finitos, ou com exploração limitada para os infinitos. Se uma invariante for violada, ele para e reporta o caminho mais curto para a falha.

Isso é força bruta, não magia. O model checker não entende sua intenção. Ele simplesmente tenta tudo. Esse é exatamente o ponto. Seus integration tests são enviesados pelas suas suposições. O model checker não tem suposições.

Especificando um protocol de consensus simples em TLA+

Vejamos um exemplo mínimo: um protocol de consensus de decreto único em que um líder propõe um valor e um quórum de aceitadores deve aceitá-lo antes de o valor ser escolhido. Essa é a ideia central por trás do Paxos, do Raft e de todo outro algoritmo de consensus de que você já ouviu falar.

Aqui está a spec TLA+ para o 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
=============================================================================

Essa spec diz: inicialmente nada é escolhido. Uma action de propor pode definir chosen para um valor único, mas apenas se ainda nada tiver sido escolhido. A invariante ChosenUniqueness estabelece que no máximo um valor pode ser escolhido.

O model checker de TLA+, o TLC, verificará que nenhum execution trace viole ChosenUniqueness. Se você introduzir um bug em que dois líderes podem propor simultaneamente sem verificar valores anteriores, o TLC encontra o contraexemplo em milissegundos.

Adicionando as partes complicadas: falhas e perda de mensagens

A spec acima é muito limpa. Sistemas distribuídos reais não são limpos. Mensagens se perdem. nodes reiniciam. partitions de rede isolam grupos de nodes uns dos outros. O modelo só se torna útil quando você modela essas falhas.

Aqui está um fragmento mais realista que modela a passagem de mensagens com perda 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 é a adição importante. Ela modela a perda de mensagens sem alterar o acceptor state. O TLC explorará traces em que qualquer mensagem é delivered, dropada ou delayed indefinidamente. Quando você adiciona uma falha e recuperação de líder, o espaço de estados cresce, mas o TLC ainda o explora sistematicamente.

Essa é a parte que me confundiu quando comecei com o TLA+. Eu queria modelar apenas a lógica do protocol. Mas os bugs não estavam na lógica. Eles estavam na interação entre a lógica e os failure modes que eu não havia considerado. Você precisa modelar ambos.

A compensação: explosão do espaço de estados e abstração

O model checking não é de graça. O número de estados cresce exponencialmente com a quantidade de processos e o tamanho dos payloads de mensagem. Uma spec com cinco valores e três aceitadores pode gerar milhões de estados. Adicione um quarto aceitador e você está em bilhões. Execute isso no seu laptop e ele ficará sem memória antes de terminar.

A solução é a abstração. Você não modela seus valores reais de 64 bytes. Você modela dois valores: V1 e V2. Se o protocol se comporta corretamente para dois valores, os valores específicos não importam. Você não modela um log de 10.000 entradas. Você modela um log de profundidade 2. Se safety se mantém for profundidade 2, quase sempre se mantém para profundidade arbitrária. Isso é chamado de small-model checking, e é a prática padrão no campo.

A habilidade chave é aprender quais detalhes importam e quais não. Os message contents geralmente não importam para as safety properties. O message ordering quase sempre importa. As node identities podem não importar, mas a contagem de nodes em cada papel importa.

Se o espaço de estados ainda for muito grande, você tem outras opções. Você pode usar symmetry reduction para tratar nodes idênticos como intercambiáveis. Você pode limitar a profundidade da busca. Ou pode mudar para um model checker simbólico como o Apalache, que usa SMT solvers para raciocinar sobre estados sem enumerá-los todos.

Da spec para a implementação: mantendo-os sincronizados

Uma spec verificada não vale nada se sua implementação divergir dela. A spec é o blueprint. O código é o edifício. Não há uma ponte automatizada entre os dois, e é nessa lacuna que os bugs voltam a se infiltrar.

A abordagem prática é tratar a spec TLA+ como um documento de design que por acaso é executável. Revise-a junto com o código durante os pull requests. Quando a implementação lida com um edge case, pergunte-se se a spec também lida. Quando você encontra um bug em produção, verifique se a spec o teria pego. Se não, atualize a spec.

Algumas equipes vão mais longe e geram test cases a partir dos counterexamples que o TLC produz. Uma trace do TLC mostrando como duas replicas divergem se torna um cenário de integration test. Isso é trabalho manual, mas conecta o modelo formal ao seu test suite.

Na Sentry, usamos essa abordagem para validar um protocol de rate limiting distribuído. A spec pegou um liveness issue em que um node em recuperação poderia sofrer starvation em um cenário de partition específico. Nossos integration tests nunca o dispararam porque sempre curavam as partitions de forma limpa. O model checker não se importava com limpo. Ele tentou o caso bagunçado, encontrou o bug e nos poupou de um incident muito confuso.

Começando: seu primeiro model check

Se você quer tentar isso, comece com a TLA+ Toolbox. É um IDE gratuito para escrever e verificar specs. Trabalhe nos exemplos de Paxos e Raft que acompanham o package. Eles são mais complexos que o snippet de consensus acima, mas mostram como protocols reais são modelados.

Para sua primeira spec, escolha algo pequeno do seu próprio sistema. Um protocol de leader election. Um esquema de cache invalidation distribuído. Uma variante de two-phase commit. Escreva as invariantes que você acredita que se mantêm. Depois deixe o TLC dizer se você está certo. Ele geralmente diz não, e geralmente diz isso dentro da primeira hora.

O model checking não encontrará todos os bugs. Não ajudará com performance, não pegará serialization mistakes e não verificará se sua implementação corresponde à sua spec. O que ele faz é encontrar os bugs profundos de protocol que os integration tests deixam passar, e os encontra no momento do design, quando as correções não custam nada.

Essa é a correção de bug mais barata em sistemas distribuídos. Não um debugger melhor. Não mais monitoring. Pegar o bug antes de o código sequer existir.