Letzte Woche erwähnte Boris Cherny, der Erfinder von Claude Code, dass Opus in der Lage war, TLA+ zu verwenden, um Race Conditions im Code zu finden. Jetzt spricht jeder über formale Verifikation. Als langjähriger Pädagoge und Befürworter von TLA+ ist das aufregend. Aber die neue Euphorie beunruhigt mich. Formale Methoden werden die agentische Softwareentwicklung nicht ein für alle Mal lösen.

Korrekte Entwürfe übersetzen sich nicht automatisch in korrekten Code. Um eine Eigenschaft zu verifizieren, brauchen wir eine zu verifizierende Eigenschaft. TLA+ unterteilt das System in Verhaltensweisen, jede eine Folge von Zuständen. In jedem Zustand können wir boolesche Ausdrücke mit drei temporalen Operatoren ausdrücken: `[]P` (immer P), `P'` (P im nächsten Zustand) und `<>P` (schließlich P).

`[]P` bedeutet, dass P in jedem Zustand jedes Verhaltens wahr ist, genannt eine Invariante. `[](x' >= x)` ist eine Aktionseigenschaft. Dies sind Sicherheitseigenschaften: etwas Schlechtes passiert nie. Lebendigkeitseigenschaften verwenden `<>`: `[]<>P` bedeutet, dass P in mindestens einem zukünftigen Zustand jedes Zustands wahr ist; `<>[]P` bedeutet, dass P wahr wird und für immer wahr bleibt; `[](P => <>Q)` bedeutet, dass P schließlich Q verursacht.