TLA+ kann nicht alles prüfen – was der Formale-Methoden-Hype übersieht
What TLA+ can and can't check
Boris Cherny, Erfinder von Claude Code, sorgte für Aufsehen, als er berichtete, dass Opus mit TLA+ Race Conditions in Code aufspüren konnte. Hillel Wayne, langjähriger TLA+-Experte, warnt jedoch vor überzogenen Erwartungen: Formale Methoden lösen nicht alle Probleme der agentischen Softwareentwicklung. Er erklärt, welche Eigenschaften TLA+ prüfen kann – Invarianten, Aktions- und Lebendigkeitseigenschaften – und welche prinzipiell nicht ausdrückbar sind, etwa Erreichbarkeitseigenschaften oder Hyperproperties.
Um eine Eigenschaft zu verifizieren, müssen wir eine Eigenschaft haben, die wir verifizieren können! Welche Eigenschaften kann TLA+ also nicht einmal ausdrücken?
- sourdecor
Ich bin durch diesen Kommentar[1] auf HN auf Quint[0] gestoßen. Quint ist "eine ausführbare Spezifikationssprache [die in JavaScript funktioniert] mit wunderbarem Tooling, basierend auf der temporalen Logik von Aktionen (TLA)". Ich finde es großartig und jeder, der sich für TLA+ interessiert, sollte es sich ansehen.
- singron
Ich liebe das. Das ist großartig zu lesen, wenn man versucht, TLA+ für etwas zu verwenden.
In eine andere Richtung: Eine weitere Sache, für die TLA+ nicht gut geeignet ist, ist die Modellierung von Atomizität und insbesondere von Weak-Memory-Semantik oder allem, was nicht sequenziell konsistent ist. Wenn man seinen Algorithmus nach pcal übersetzt, läuft er so, als wäre er sequenziell konsistent. Wenn man Nicht-Sequenzielle-Konsistenz modellieren muss, dann muss das mit expliziter Logik in TLA+ ausgedrückt werden, was wahrscheinlich zu kompliziert und fehleranfällig ist, um es von Hand zu machen. Die Speichermodelle von C/C++/Rust erlauben eine Menge verrückter Sachen. Ich stelle mir vor, dass man für jede Variable Read-Caches und Writeback-Buffer mit Cache-Flushing-Anweisungen an geeigneten Stellen hinzufügen muss, aber vielleicht gibt es einen eleganteren Weg.
Wenn man Rust verwendet, haben miri und loom beide Analyzer, die einige nicht-sequenziell-konsistente Verhaltensweisen prüfen können (und loom implementiert tatsächlich überhaupt keine Sequenzielle Konsistenz).
- adamddev1
Großartiger Artikel. Die Leute sagen immer wieder "wir können einfach Tests schreiben" oder in jüngerer Zeit "wir können formale Verifikation verwenden", und denken, das seien ausreichende Schutzmaßnahmen, die wir nutzen können, um dann die gesamte Implementierung an LLMs zu delegieren. Aber Tatsache ist, dass probabilistische Rate-Maschinen sie nicht retten können. Die Menschen können nicht der Notwendigkeit entgehen, die Dinge, die sie bauen, tatsächlich zu verstehen.
- rrook
Ich denke, ein Teil davon ist eine Schwäche unserer Programmiersprachen. Im Allgemeinen erlauben Sprachen die Darstellung partieller Graphen, was das Verifikationsproblem technisch anspruchsvoll macht. Meiner Meinung nach könnte eine Sprache, die nur Closed-Graph-Semantik bietet, helfen, die Lücke zwischen Modell und Implementierung zu schließen, auch wenn nicht absolut.
- metabagel
Ich liebe die Inline-Fußnoten!