Du kannst ein verteiltes protocol nicht unit-testen. Ein Unit Test führt einen Prozess auf einer Maschine in einer bestimmten Reihenfolge aus. Dein protocol läuft auf zehn Prozessen über fünf Maschinen in einer Reihenfolge, die du nicht kontrollierst. Die Lücke zwischen diesen beiden Realitäten ist dort, wo deine Bugs leben.

Model Checking schließt diese Lücke. Es erkundet jede mögliche Verschränkung jedes möglichen Zustands, den dein protocol erreichen kann. Wenn es einen Weg gibt, bei dem zwei replicas nicht übereinstimmen, einen Weg, bei dem eine Leader Election in einen Deadlock gerät, oder einen Weg, bei dem ein Split-Brain-Szenario auftritt, findet ein Model Checker ihn. Und zwar bevor du den ersten RPC Handler geschrieben hast.

Warum verteilte Bugs traditionelles Testing überleben

State Explosion ist das Problem. Drei Nodes, die Nachrichten austauschen, können Milliarden von Ausführungspfaden erzeugen. Handgeschriebene Integration Tests decken vielleicht ein Dutzend davon ab, meist den Happy Path und ein paar offensichtliche Failure Modes. Der Bug, bei dem Node A genau zwischen dem Senden eines Prepare und einem Ack abstürzt? Viel Glück, den in CI zu treffen.

Formale Verifikation klingt nach einer akademischen Übung, aber Model Checking ist anders. Du beweist nicht, dass das protocol für alle Zeit korrekt ist. Du beschreibst das protocol in einer Specification Language, definierst die Eigenschaften, die dir wichtig sind, und lässt ein Tool den State Space bis zu einer bestimmten Grenze erschöpfend durchsuchen. Wenn es eine Verletzung findet, liefert es dir eine minimale Trace. Du bekommst ein Schritt-für-Schritt-Rezept zur Reproduktion des Bugs. Keine Heisenbugs. Kein „funktioniert auf meiner Maschine“.

Das praktischste Tool dafür ist TLA+, entwickelt von Leslie Lamport. Es sieht aus wie Mathe, weil es Mathe ist. Aber die Mathe ist einfacher, als du erwartest, und der Payoff ist, Bugs zu finden, die sonst um 2 Uhr nachts in Produktion auftauchen würden.

Was Model Checking tatsächlich macht

Ein Model Checker nimmt drei Inputs: eine Beschreibung deines Systems, eine Beschreibung seiner Umgebung und die Eigenschaften, die gelten sollen. Die Systembeschreibung erfasst deine protocol logic. Die Umgebungsbeschreibung erfasst alles, was du nicht kontrollierst: Netzwerk-Delays, Message Loss, Node Crashes, Clock Skew. Die Eigenschaften sind meist Invarianten („das committed Log wird niemals überschrieben“) oder Liveness Conditions („jede Request bekommt irgendwann eine Response“).

Der Checker generiert dann jeden erreichbaren Zustand und jeden gültigen Übergang zwischen ihnen. Er macht dies erschöpfend für finite State Spaces oder mit bounded exploration für infinite. Wenn eine Invariante verletzt wird, stoppt er und meldet den kürzesten Pfad zum Failure.

Das ist Brute Force, keine Magie. Der Model Checker versteht deine Absicht nicht. Er probiert einfach alles aus. Genau das ist der Punkt. Deine Integration Tests sind durch deine Annahmen verzerrt. Der Model Checker hat keine Annahmen.

Spezifikation eines einfachen consensus protocol in TLA+

Schauen wir uns ein minimales Beispiel an: ein Single-Decree-consensus protocol, bei dem ein Leader einen Wert vorschlägt und ein Quorum von Acceptors ihn akzeptieren muss, bevor der Wert gewählt wird. Das ist die Kernidee hinter Paxos, Raft und jedem anderen Consensus Algorithmus, von dem du je gehört hast.

Hier ist die TLA+ Spec für das System:

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

Diese Spec sagt: Anfangs ist nichts gewählt. Eine Propose action kann chosen auf einen einzelnen Wert setzen, aber nur, wenn noch nichts gewählt wurde. Die ChosenUniqueness-Invariant besagt, dass höchstens ein Wert jemals gewählt werden kann.

Der TLA+ Model Checker, TLC, wird verifizieren, dass keine Execution Trace ChosenUniqueness verletzt. Wenn du einen Bug einführst, bei dem zwei Leader gleichzeitig vorschlagen können, ohne vorherige Werte zu prüfen, findet TLC das Gegenbeispiel in Millisekunden.

Hinzufügen der unangenehmen Teile: Crashes und Message Loss

Die obige Spec ist zu sauber. Echte verteilte Systeme sind nicht sauber. Nachrichten gehen verloren. Nodes starten neu. Network Partitions isolieren Gruppen von Nodes voneinander. Das Modell wird erst nützlich, wenn du diese Failures modellierst.

Hier ist ein realistischeres Fragment, das Message Passing mit potenziellem Verlust modelliert:

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 ist die wichtige Ergänzung. Sie modelliert Message Loss, ohne den Acceptor State zu ändern. TLC wird Traces erkunden, in denen jede Nachricht delivered, gedroppt oder unendlich lange delayed wird. Wenn du einen Leader Crash und Recovery hinzufügst, wächst der State Space, aber TLC erkundet ihn immer noch systematisch.

Das ist der Teil, der mich am Anfang bei TLA+ verwirrt hat. Ich wollte nur die protocol logic modellieren. Aber die Bugs steckten nicht in der Logik. Sie steckten in der Interaktion zwischen der Logik und Failure Modes, die ich nicht bedacht hatte. Du musst beides modellieren.

Der Trade-off: State Space Explosion und Abstraktion

Model Checking ist nicht kostenlos. Die Anzahl der Zustände wächst exponentiell mit der Anzahl der Prozesse und der Größe deiner Nachrichten-Payloads. Eine Spec mit fünf Werten und drei Acceptors könnte Millionen von Zuständen erzeugen. Füge einen vierten Acceptor hinzu, und du bist bei Milliarden. Führe das auf deinem Laptop aus, und er geht dem Speicher aus, bevor er fertig ist.

Die Lösung ist Abstraktion. Du modellierst nicht deine tatsächlichen 64-Byte-Werte. Du modellierst zwei Werte: V1 und V2. Wenn das protocol für zwei Werte korrekt funktioniert, spielen die spezifischen Werte keine Rolle. Du modellierst kein 10.000-Einträge-Log. Du modellierst ein Log der Tiefe 2. Wenn Safety für Tiefe 2 gilt, gilt sie fast immer für beliebige Tiefe. Das nennt man Small-Model Checking, und es ist Standard in diesem Feld.

Die Schlüsselkompetenz ist, zu lernen, welche Details wichtig sind und welche nicht. Message Contents spielen für Safety Properties meist keine Rolle. Message Ordering spielt fast immer eine Rolle. Node Identities könnten keine Rolle spielen, aber die Anzahl der Nodes in jeder Rolle schon.

Wenn der State Space immer noch zu groß ist, gibt es andere Optionen. Du kannst Symmetry Reduction verwenden, um identische Nodes als austauschbar zu behandeln. Du kannst die Suchtiefe begrenzen. Oder du wechselst zu einem symbolischen Model Checker wie Apalache, der SMT Solvers verwendet, um über Zustände zu reasoning, ohne sie alle aufzuzählen.

Von der Spec zur Implementierung: Synchronisation aufrechterhalten

Eine verifizierte Spec ist wertlos, wenn deine Implementierung davon abweicht. Die Spec ist der Blueprint. Der Code ist das Gebäude. Es gibt keine automatisierte Brücke zwischen den beiden, und in dieser Lücke schleichen sich Bugs wieder ein.

Der praktische Ansatz ist, die TLA+ Spec als Design Document zu behandeln, das zufällig ausführbar ist. Reviewe sie zusammen mit dem Code während Pull Requests. Wenn die Implementierung einen Edge Case behandelt, frag dich, ob die Spec ihn auch behandelt. Wenn du einen Bug in Produktion findest, prüfe, ob die Spec ihn gefangen hätte. Wenn nicht, aktualisiere die Spec.

Manche Teams gehen weiter und generieren Test Cases aus den Counterexamples, die TLC produziert. Eine TLC Trace, die zeigt, wie zwei replicas divergieren, wird zu einem Integration-Test-Szenario. Das ist manuelle Arbeit, aber sie verbindet das formale Modell mit deiner Test Suite.

Bei Sentry haben wir diesen Ansatz verwendet, um ein verteiltes rate-limiting protocol zu validieren. Die Spec hat ein Liveness Issue gefangen, bei dem ein sich erholender Node in einem bestimmten Partition Szenario verhungern konnte. Unsere Integration Tests hatten es nie getriggert, weil sie Partitionen immer sauber geheilt haben. Der Model Checker kümmerte sich nicht um sauber. Er probierte den unordentlichen Fall, fand den Bug und ersparte uns einen sehr verwirrenden Incident.

Erste Schritte: Dein erstes Model Check

Wenn du das ausprobieren willst, starte mit der TLA+ Toolbox. Es ist eine kostenlose IDE zum Schreiben und Prüfen von Specs. Arbeite die Paxos- und Raft-Beispiele durch, die mitgeliefert werden. Sie sind komplexer als das Consensus-Snippet oben, aber sie zeigen, wie echte protocols modelliert werden.

Für deine erste Spec wähle etwas Kleines aus deinem eigenen System. Ein leader election protocol. Ein verteiltes Cache-Invalidation-Schema. Eine Two-Phase-Commit-Variante. Schreibe die Invarianten auf, von denen du glaubst, dass sie gelten. Dann lass TLC dir sagen, ob du recht hast. Es sagt meist nein, und es sagt es meist innerhalb der ersten Stunde.

Model Checking findet nicht jeden Bug. Es hilft nicht bei Performance, es fängt keine Serialization Mistakes, und es verifiziert nicht, dass deine Implementierung deiner Spec entspricht. Was es tut, ist, die tiefen protocol bugs zu finden, die Integration Tests verpassen, und es findet sie zur Design-Zeit, wenn Fixes nichts kosten.

Das ist die billigste Bug-Fix in verteilten Systemen. Kein besserer Debugger. Kein mehr Monitoring. Den Bug zu fangen, bevor der Code überhaupt existiert.