Boris Cherny, der Kopf hinter Claude Code, machte letzte Woche eine unauffällige Ankündigung. Er sagte, Opus habe TLA+ verwendet, um Race Conditions im Code zu finden. Seitdem spricht das gesamte Internet über formale Verifikation. Das ist die Geschichte, und es ist eine gute – aber sie kommt mit einer Einschränkung. TLA+ ist hervorragend geeignet für die Gestaltung komplexer nebenläufiger Systeme und um sicherzustellen, dass diese fehlerfrei sind. Es ist kein Allheilmittel.
Wie TLA+ ein System aufbricht
TLA+ funktioniert, indem es ein System in eine Reihe von Verhaltensweisen aufteilt. Jedes Verhalten ist eine Folge von Zuständen, wie „Ampel eins ist grün, dann gelb, dann rot.“ Innerhalb jedes Zustands können Sie einfache boolesche Ausdrücke schreiben: „Ampel vier ist grün“ oder „Alle Ampeln sind rot.“ Dann fügen Sie drei temporale Operatoren hinzu:
[]P(„always P“) is true if P holds in the current state and every future state.P'(„P prime“) is true if P holds in the next state.<>P(„eventually P“) is true if P holds in the current state or at least one future state.
These operators let you build invariants, which are properties that hold across every state of every behavior. For example, []P means P is true in every initial state, and then by definition it stays true in every future state. That’s a safety property — something bad never happens. Liveness is the opposite: „something good always happens.“ It’s built around <>P, but <>P alone is usually too weak. Combinations like []<>P and <>[]P make the logic richer.
There are also other operators like ENABLED and <<A>>_v. Most of what TLA+ checks falls into invariants, action properties, and liveness. Refinement combines safety and liveness and is a whole topic unto itself.
Die Eigenschaften, die TLA+ nicht prüfen kann
Der Haken ist, dass TLA+ Eigenschaften nicht prüfen kann, die es nicht einmal ausdrücken kann. Wenn Sie nicht wissen, wie Sie Ihre Eigenschaft als logische Formel darstellen, kann TLA+ nicht helfen. Das ist kein Fehler in TLA+ — es ist eine Grenze formaler Methoden im Allgemeinen. Wenn Sie den menschlichen Begriff eines Vogels nicht formalisieren können, können Sie nicht beweisen, dass Ihre App Vögel erkennt.
Einige Eigenschaften fallen in diese Kategorie. Erreichbarkeitseigenschaften sind ein Beispiel. Sie können nicht beweisen, dass ein Spiel gewinnbar ist, oder dass P von jedem Anfangszustand aus erreichbar ist, oder dass P von jedem Zustand aus erreichbar ist, in dem Q wahr ist. Diese werden Erreichbarkeitseigenschaften genannt.
Eine weitere Grenze ist die Spezifität. TLA+-Sicherheitseigenschaften funktionieren mit einzelnen Zuständen oder einzelnen Schritten. Sie können keine Eigenschaft über zwei oder mehr Schritte definieren, wie z. B. „Löschen und dann Rückgängig machen gibt Ihnen den ursprünglichen Zustand zurück.“ Sie können keine Eigenschaften für Gleitkommaoperationen oder über Realzeit definieren — nur über logische Zeit. Hyper-Eigenschaften sind ein weiterer blinder Fleck. Sie können keine Eigenschaften über eine Menge von Verhaltensweisen definieren. Zum Beispiel können Sie keine Telefonhardware modellieren, bei der Sie etwas darüber aussagen wollen, wie mehrere Verhaltensweisen interagieren.
Die Kernbeschränkung
The most interesting limit, according to the author, is implicit quantification. TLA+ properties are implicitly quantified over all behaviors. Checking []P means „for all behaviors, []P is true of that behavior’s initial state.“ Any property TLA+ can check must be true for every individual behavior. That means you can’t say „there exists a behavior where P is true.“
Das lässt viel aus. Sie können nicht beweisen, dass P möglich ist, selbst wenn Sie es nicht tatsächlich erreichen. Sie können keine Eigenschaften über eine Menge von Verhaltensweisen definieren. Der Autor nennt diese Hyper-Eigenschaften.
Warum das jetzt wichtig ist
Die Begeisterung rund um TLA+ ist verständlich. Cherny’s Ankündigung zeigte, dass ein echtes Werkzeug echte Fehler finden kann. Aber die Hype-Maschinerie hat die Angewohnheit, Einschränkungen hinwegzuschlucken. Der Autor befürchtet, dass Leute sagen, formale Methoden werden das Problem der agenturbasierten Softwareentwicklung einmal und für alle lösen. Das ist Unsinn.
Die Schwächen von TLA+ sind gut dokumentiert. Korrekte Designs lassen sich nicht automatisch in korrekten Code übersetzen. Aber dieser Newsletter konzentriert sich auf eine andere Einschränkung: Um eine Eigenschaft zu verifizieren, benötigt man eine Eigenschaft, die man verifizieren kann. Wenn man die Eigenschaft nicht ausdrücken kann, kann kein Werkzeug sie prüfen.
Der Autor ist ein langjähriger Pädagoge und Verfechter von TLA+. Sie sind außerdem ein langjähriger Verfechter von Besonnenheit. Die neue Euphorie beunruhigt sie.
Was man daraus mitnehmen kann
Die Aussage ist nicht, dass TLA+ nutzlos ist. Es ist, dass es präzise ist. Seine Grenzen sind bekannt. Die Eigenschaften, die es nicht prüfen kann, sind die Eigenschaften, die es nicht prüfen kann – und das ist eine Stärke, kein Scheitern.
Die eigene Position des Autors ist verspielt und ehrlich. Sie halten sowohl das Versprechen des Titels ein: was TLA+ prüfen kann und was es nicht kann.
TLA+ ist hervorragend geeignet, um komplexe nebenläufige Systeme zu entwerfen und sicherzustellen, dass sie fehlerfrei sind. Es ist kein Zauberstab für alles. Der beste Weg, es zu verwenden, ist zu wissen, was es gut kann und was es nicht berührt.
Ein letzter Hinweis: Der Autor ist ein langjähriger Pädagoge und Verfechter von TLA+. Sie sind außerdem ein langjähriger Verfechter von Besonnenheit. Ihre Befürchtung ist, dass die neue Euphorie rund um das Werkzeug die Einschränkungen übertönt. Das ist erwähnenswert, während die Diskussion weitergeht.
Quellenmaterial: „What TLA+ can and can’t check,“ buttondown.com.
Das Notizbuch abonnieren.
Die besten Geschichten des Tages und jedes neue Urteil, in klarem Deutsch, um sieben im Postfach. Eine Mail am Tag, nicht mehr.