KI wird formale Verifikation in den Mainstream bringen
(martin.kleppmann.com)- Formale Verifikation (formal verification) ist eine Methode, mathematisch zu beweisen, dass Code eine Spezifikation stets erfüllt, und blieb lange auf einen begrenzten, forschungsnahen Bereich beschränkt
- Einige große Systeme wie der seL4-Mikrokernel wurden mithilfe formaler Verifikation entwickelt, doch wegen des hohen Schwierigkeitsgrads und der hohen Kosten wurde sie in der Industrie kaum eingesetzt
- In jüngster Zeit zeigen LLM-basierte Coding-Assistenten nicht nur bei Implementierungscode, sondern auch beim Schreiben von Beweisskripten in verschiedenen Sprachen Erfolge, was das Kostenmodell der Verifikation grundlegend verändern könnte
- Wenn KI neben der Codegenerierung auch den Korrektheitsbeweis automatisieren kann, könnte sich die Softwareentwicklung zu einem verlässlicheren Ansatz als menschliches Code-Review wandeln
- Die Automatisierung formaler Verifikation ist eine Schlüsseltechnologie zur Sicherung der Softwarezuverlässigkeit im KI-Zeitalter; für die breite Etablierung dürfte weniger die Technik als vielmehr ein kultureller Wandel entscheidend sein
Aktueller Stand und Grenzen der formalen Verifikation
- Beweisorientierte Sprachen und Werkzeuge wie Rocq, Isabelle, Lean, F*, Agda ermöglichen es, mathematisch zu beweisen, dass Code eine Spezifikation erfüllt
- Der seL4-Betriebssystemkernel, der CompCert-C-Compiler und der Kryptoprotokoll-Stack Project Everest sind typische Beispiele
- In der Industrie wird formale Verifikation jedoch kaum verwendet
- Bei seL4 waren für die Verifikation von 8.700 Zeilen C-Code 20 Personenjahre und 200.000 Zeilen Isabelle-Code nötig
- Pro Zeile Implementierung waren 23 Zeilen Beweis und ein halber Personentag Arbeit erforderlich
- Weltweit gibt es Schätzungen zufolge nur einige Hundert Experten, die solche Beweise schreiben können
- Auch wirtschaftlich waren bei den meisten Systemen die Verifikationskosten höher als die Verluste durch Bugs, weshalb die praktische Nutzbarkeit gering war
Wie KI die Wirtschaftlichkeit formaler Verifikation verändert
- In jüngster Zeit zeigen LLM-basierte Coding-Assistenten nicht nur bei Implementierungscode, sondern auch beim Schreiben von Beweisskripten Erfolge
- In Nature, bei Galois, auf arXiv usw. wurden Fälle berichtet, in denen LLMs Beweise in mehreren Sprachen erzeugt haben
- Derzeit ist noch Anleitung durch Experten nötig, doch eine vollständige Automatisierung scheint in den nächsten Jahren möglich
- Wenn die Verifikationskosten stark sinken, kann formale Verifikation auf deutlich mehr Software angewendet werden
- Gleichzeitig braucht von KI erzeugter Code formale Verifikation statt menschlicher Prüfung, um Zuverlässigkeit sicherzustellen
- Wenn KI die Korrektheit ihres Codes selbst beweisen kann, könnte er gegenüber handgeschriebenem Code bevorzugt werden
Die komplementäre Beziehung zwischen LLMs und Beweisprüfung
- Wenn LLMs Beweisskripte schreiben, können sie zwar Falschinhalte (Halluzinationen) erzeugen, doch ein Proof Checker weist diese zurück
- Der Checker besteht selbst aus kleinem, eigenständig verifiziertem Code, sodass falsche Beweise nur schwer akzeptiert werden können
- Dadurch ergänzt die Strenge formaler Verifikation die Unsicherheit von LLMs
- Diese Kombination bildet einen sicheren Automatisierungspfad, um die Zuverlässigkeit von KI-generiertem Code sicherzustellen
Neue Herausforderung: die Korrektheit der Spezifikation
- Auch in einer automatisierten Verifikationsumgebung bleibt die korrekte Definition der Spezifikation (specification) die zentrale Aufgabe
- Es muss überprüft werden, ob die bewiesenen Eigenschaften tatsächlich den vom Entwickler beabsichtigten Eigenschaften entsprechen
- Das Schreiben von Spezifikationen erfordert weiterhin Fachwissen und sorgfältiges Nachdenken, ist aber deutlich einfacher und schneller als manuelle Beweise
- KI könnte auch die Übersetzung von Spezifikationen zwischen natürlicher Sprache und formalen Sprachen unterstützen
- Allerdings besteht das Risiko von Bedeutungsverlusten, das jedoch als beherrschbar eingeschätzt wird
Ausblick auf Veränderungen in der Softwareentwicklung
- Entwickler könnten die gewünschten Eigenschaften des Codes deklarativ als Spezifikation beschreiben, während KI Implementierung und Beweis gemeinsam erzeugt
- In diesem Fall müssten Entwickler den von der KI erzeugten Code nicht mehr direkt prüfen und könnten ihn ähnlich vertrauensbasiert wie Maschinencode aus dem Compiler verwenden
- Zusammengefasst sind die folgenden drei Veränderungen zu erwarten
- Ein drastischer Rückgang der Kosten formaler Verifikation
- Eine steigende Nachfrage nach Verifikation, um das Vertrauen in KI-generierten Code sicherzustellen
- Die Präzision formaler Verifikation ergänzt die probabilistische Natur von LLMs
- Wenn diese Faktoren zusammenwirken, ist es sehr wahrscheinlich, dass formale Verifikation zu einer Mainstream-Technologie des Software Engineering wird
- Künftige Begrenzungsfaktoren dürften weniger technischer Natur sein als vielmehr die Geschwindigkeit, mit der Entwicklungskulturen den Wandel annehmen
1 Kommentare
Hacker-News-Kommentare
Ich denke, formale Verifikation (formal verification) zeigt ihren wahren Wert in Bereichen, in denen die Implementierung viel komplexer ist als die Spezifikation.
Zum Beispiel bei bitgenauen Optimierungen in Kryptografie-Implementierungen oder in Compiler-Optimierungsphasen.
Aber der Code, den die meisten Entwickler:innen (oder AIs) schreiben, ist dank Hochsprachen bereits recht nah an der Spezifikation, daher halte ich den Nutzen formaler Verifikation oft für begrenzt.
Ich bin mir auch nicht sicher, ob eine separat geschriebene Spezifikation wirklich leichter zu lesen wäre.
Schon heute abstrahieren verschiedene Frameworks und Bibliotheken viele Implementierungsdetails.
Formale Verifikation kann zwar stärkere Garantien liefern, aber die meisten Menschen wollen dieses Niveau an Garantien gar nicht, und ich glaube auch nicht, dass AI dafür plötzlich einen neuen Bedarf schaffen wird.
Manche sagen voraus, dass AI die formale Verifikation vollständig automatisieren wird, aber ich halte diese Logik für problematisch.
Wenn AI Software automatisch beweisen kann, muss von Menschen geschriebene Software vielleicht gar nicht mehr verifiziert werden.
AI könnte dann selbst Ideen entwerfen, implementieren und das gewünschte Verifikationsniveau festlegen.
Letztlich könnten menschliches Programmieren und menschliche Verifikation weitgehend verschwinden.
Es ist zwar möglich, dass Menschen einen Proof Assistant entwerfen, aber ihn zur Verifikation großer Programme zu nutzen, ist viel schwieriger.
Wenn eine solche AI also auftaucht, könnte sie vermutlich auch selbst neue Proof Assistants entwickeln.
Natürlich ist das eher Science-Fiction; solange wir nicht klar wissen, was AI leichter oder schwerer machen wird, haben solche Vorhersagen wenig Bedeutung.
Link zur verwandten Diskussion
Das wäre wohl ein Wendepunkt, an dem die Menschheit in eine völlig andere Phase eintritt.
Um mit Coding Agents (Claude Code, Codex CLI usw.) nützliche Ergebnisse zu bekommen, ist es entscheidend, eine Umgebung bereitzustellen, in der ihr Code ausgeführt und verifiziert werden kann.
Sprachen wie Python, die sich leicht ausführen lassen, sind dafür am besten geeignet; bei HTML+JS braucht man Werkzeuge wie Playwright.
Der nächste Schritt sind automatisierte Test-Suiten sowie Qualitätswerkzeuge wie Code Formatter, Linter und Fuzzer.
Ein Debugger ist auch gut, aber weil er interaktiv ist, ist er für Agents schwerer zu nutzen.
Ich denke, auch Werkzeuge zur formalen Verifikation gehören in dieses Spektrum — heutige Modelle kommen schließlich auch mit speziellen Programmiersprachen gut zurecht.
Wenn dir Coding Agents wenig nützlich erscheinen, liegt das wahrscheinlich daran, dass eine Ausführungs- und Testumgebung fehlt.
Bei Haskell zum Beispiel gilt oft: Wenn es kompiliert, funktioniert es fast immer richtig.
Wenn diese Eigenschaft für Menschen nützlich ist, dann gilt das auch für LLMs.
Besonders Property Tests passen gut zu LLMs — mit wenigen Tests kann man einen großen Fehlerraum abdecken.
Wenn man sieht, dass die Mathematik-Community versucht, LLMs zur Verbesserung von Lean-Code einzusetzen, scheint auch Softwareentwicklung mit stärkeren Typsystemen durchaus realistisch.
Debugging ist nicht sequenziell, und Ursache und Wirkung liegen zeitlich oft durcheinander.
Als ich früher mit gdb einen Multithreading-Bug gejagt habe, habe ich auch ChatGPT ausprobiert, aber es schlug immer nur vor, noch ein paar
print-Ausgaben hinzuzufügen.Das hat mir erneut gezeigt, dass dies ein Bereich ist, in dem Erfahrung und Intuition nötig sind.
Es wäre absurd, von einem Junior Engineer zu erwarten, ohne Debugger oder Test Runner zu arbeiten.
Letztlich wird man wohl mehr Rechenressourcen brauchen.
Claude implementiert, Codex und Gemini reviewen.
Das ist teuer, aber es war für mich der sicherste Weg, Self-Bias zu reduzieren und die Codequalität zu erhöhen.
Werkzeuge zur statischen Analyse würden zusätzlich helfen, aber nur immer mehr Tools hinzuzufügen, reicht meiner Meinung nach nicht.
Wenn der Verifikationsprozess automatisiert wird, verlagert sich der wirklich schwierige Teil auf die präzise Definition der Spezifikation (specification).
Das Schreiben der Spezifikation ist viel schneller und leichter als der Beweis selbst, erfordert aber weiterhin Fachwissen und Sorgfalt.
Dass sich formale Beweise in der Vergangenheit nicht verbreitet haben, lag nicht nur an ihrer Schwierigkeit, sondern auch daran, dass das Wasserfall-Modell verschwand und agile Entwicklung zum Mainstream wurde.
Statt lange Spezifikationen zu schreiben, hat sich die Praxis hin zu schnellen Iterationen entlang der Nutzeranforderungen entwickelt.
Es scheint Zeit zu sein, OCaml zu lernen.
Viele Proof Assistants und Verifikationssysteme können OCaml-Code erzeugen, und auch ADA/Spark ist einen Blick wert.
Software Engineering wird sich im AI-Zeitalter so oder so verändern, aber wir müssen Software von höherer Qualität bauen als heute.
Formale Verifikation wird dabei sicher helfen.
Es ist noch unfertig, aber ich teile mein Experimentierprojekt.
In einer Welt mit zu wenig codezentrierten Texten könnte es für jemanden, der nach einer interessanten Hackathon-Idee sucht, nützlich sein.
Link zum Projekt py-mcmas
LLMs neigen dazu, Probleme gut zu lösen, die sich leicht verifizieren lassen.
Deshalb teile ich Problemlösung in drei Schritte auf.
1️⃣ Zuerst schreibe ich ein Programm für die Erfolgsbedingungen,
2️⃣ dann lasse ich damit das ursprüngliche Problem verifizieren,
3️⃣ und zuletzt prüfe ich es selbst noch einmal.
Das ist ein Ansatz, den ich schon lange verwende, aber inzwischen erledigen Modelle wie Opus oder GPT-5.2 das auch im unbeaufsichtigten Modus sehr gut.
Zugehöriger Blogbeitrag
In Bereichen, in denen Verifikation lange dauert, kann das am Ende sogar nur die menschliche Prüfungsarbeit erhöhen.
Es kann natürlich die Frage aufkommen: „Wer verifiziert das Verifikationsprogramm?“
Wenn das ebenfalls von einem LLM geschrieben wird, kann das wie ein endloser Turm von Schildkröten (turtles all the way down) wirken.
Schwierig ist es, den Beweis überhaupt zu erzeugen.
Natürlich gibt es bei komplexen Aussagen Ausnahmen, aber zur Verringerung von Bugs hilft das enorm.
Auch wenn formale Verifikation breiter eingesetzt wird, werden wohl nicht plötzlich alle Lean oder Isabelle verwenden.
Wahrscheinlicher ist, dass AI sie nahtlos in bestehende Workflows einbettet.
Zum Beispiel als Eigenschaftsprüfung in CI oder als Button im IDE nach dem Motto „Beweise die Invariante dieses Moduls“.
Die meisten Engineers werden Proof Scripts wahrscheinlich nie direkt sehen müssen.
Die eigentliche Schwierigkeit besteht nicht darin, dass LLMs Beweise erzeugen, sondern Organisationen dazu zu bringen, in das Schreiben von Spezifikationen und Modellen zu investieren.
Wenn AI das Vorschlagen und Überarbeiten von Spezifikationen einfacher macht, könnte Verifikation sich ganz natürlich wie Tests oder Linter als Refactoring-Werkzeug etablieren.
Manche beschweren sich, dass GPT‑5.2 nicht einmal richtig zählen könne, wie viele r in „garlic“ stecken.
Wenn es wirklich nötig ist, lässt man das LLM einfach ein Python-Skript schreiben und ausführen.
Sie ist nicht ganz falsch, betrifft aber nur Implementierungsdetails der Tokenisierung und hat mit der tatsächlichen Nützlichkeit fast nichts zu tun.
Es gibt kaum Situationen, in denen man ein LLM dafür benutzen würde, Buchstaben in einem Wort zu zählen.