Stephan Schmidt - June 15, 2026

KI und Formale Beweise - ein Comeback?

Warum KI Formale Beweise billig macht und die eigentliche Frage – was überhaupt bewiesen werden soll – so schwer bleibt wie 1986

Alle schreiben gerade über den Post von Jane Street – ein Tradinghaus, das fünfundzwanzig Jahre lang skeptisch auf formale Methoden geschaut hat und jetzt, getrieben von agentischem Coding, ein eigenes Team dafür aufbaut –, und seitdem fällt in jedem zweiten Gespräch über KI und Engineering derselbe Satz, mal vom CTO, mal von einem Berater auf der Bühne, mal von jemandem, der den Post nur überflogen hat: „Jetzt ist endlich die Zeit für formale Verifikation." Der Ton ist fast immer gleich, eine Mischung aus echter Begeisterung und einer leisen Angst, die selten ausgesprochen wird – die Angst, einen Moment zu verpassen, der nur einmal kommt, ein Now-or-never, nach dem die Konkurrenz beweist, während du noch testest.

Und ja, da ist was dran. Die KI schreibt dir heute in Minuten die Annotationen hin, an denen formale Verifikation dreißig Jahre lang gestorben ist, und das verändert wirklich etwas. Es verändert nur etwas anderes, als die Konferenzfolien behaupten, und wer am falschen Ende sucht, hat am Ende ein grünes Häkchen im CI und keine Ahnung, ob dahinter je jemand die Wahrheit gemeint hat.

Was die KI wirklich wegnimmt

Teuer an der formalen Verifikation war immer das Annotieren, das geduldige Hinschreiben von Invarianten und Vor- und Nachbedingungen, das Übersetzen einer Absicht in eine Sprache, die ein Verifizierer überhaupt versteht, und an dieser Fleißarbeit sind ganze Projekte gescheitert, lange bevor der erste Beweis lief – genau die übernimmt die KI jetzt, geduldig und in einem Tempo, das vorher niemand für eine ganze Codebase aufgebracht hätte. Dazu kommt eine Arbeitsteilung, die wirklich elegant ist: Das Modell ist der billige Erzeuger, der schlampen und halluzinieren darf, und der formale Verifizierer ist der teure, langsame, sound Prüfer, der durchwinkt, was hält, und liegen lässt, was bricht, sodass der Erzeuger sich irren darf, solange der Prüfer wach bleibt. Und das ist kein akademisches Spielzeug: Gobra, ein modularer separationslogischer Verifizierer für Go, hat den SCION-Router abgesichert, ein echtes Internet-Routing-Protokoll im Produktionseinsatz, kein Lehrbuchbeispiel mit drei Zeilen und einem Pfeil.

Genau diese saubere Arbeitsteilung führt dich in die Falle.

Was heißt überhaupt korrekt?

Das Schwere an der Verifikation war immer die Frage davor, die so harmlos aussieht, dass man sie überspringt: Was heißt eigentlich korrekt? Schreibt dieselbe Instanz – dasselbe Modell, in derselben Sitzung, aus demselben Weltbild heraus – sowohl den Code als auch die Spezifikation, und stimmen beide am Ende sauber überein, dann hast du nur eines gezeigt: dass der Code zu der Vorstellung von Korrektheit passt, die die KI sowieso schon hatte; über die Wirklichkeit sagt das gar nichts. Müll rein, Müll raus, diesmal mit grünem Häkchen drauf.

Das ist gefährlicher als gar keine Verifikation, weil das grüne Häkchen die kritische Prüfung beendet, bevor sie anfängt – wer schaut schon ein zweites Mal hin, wenn der Beweis doch durchgelaufen ist. Billiger geworden ist das Beweisen, und das ist echter Fortschritt. Die Frage davor kostet dich genau so viel wie immer: zu entscheiden, was überhaupt zugesichert werden soll, und ob das, was du zusicherst, irgendetwas mit dem zu tun hat, was die Welt von deinem System verlangt.

Der naheliegende Ausweg, und warum er 1986 schon scheiterte

Der Reflex ist naheliegend: Dann nimm eben eine zweite KI für die Spezifikation, lass zwei Modelle gegeneinander laufen, Redundanz, Mehrheitsentscheid, fertig. Das klingt nach sauberem Ingenieursdenken, nach redundanten Systemen und Voting. Diese Hoffnung wurde schon einmal geprüft, sauber und empirisch und mit echtem Code, lange bevor das Wort Prompt existierte.

Die Idee heißt N-Version-Programming, vorgeschlagen 1977 von Chen und Avižienis, und ihre tragende Annahme war, dass unabhängig entwickelte Programme auch unabhängig voneinander ausfallen, sodass ein Mehrheitsentscheid die Fehler herausfiltert. Knight und Leveson haben diese Annahme 1986 geprüft, und der Aufbau ist bis heute mein liebstes Argument gegen zu schnelle Redundanz: 27 unabhängig entwickelte Versionen aus derselben Spezifikation, geschrieben an zwei verschiedenen Universitäten, durchgejagt durch eine Million Testfälle, jede einzelne Version für sich hochzuverlässig – und trotzdem versagten sie gemeinsam, bei denselben Eingaben, deutlich häufiger, als statistische Unabhängigkeit es je erlaubt hätte. Der Grund dahinter gilt weit über das Experiment hinaus: Eine schwierige Stelle im Problem ist für alle schwierig, ganz gleich wie viele Teams unabhängig daran sitzen, und deshalb stolpern sie alle an genau derselben Stelle, ohne sich je abgesprochen zu haben. Der Befund war kein Zufall, er wurde mit zwanzig Versionen über mehrere Universitäten repliziert und nie widerlegt, und er steht seitdem als Standardwarnung gegen die schöne Idee, dass Vielfalt von allein Unabhängigkeit kauft.

Eine zweite KI ist heute ein zweites Team mit geteilten Trainingsdaten und geteilten blinden Flecken, und damit korrelieren ihre Fehler sogar stärker als bei zwei menschlichen Teams. Echte Unabhängigkeit holst du dir von einer anderen Abstraktionsebene – einer deklarativen Spec, einer externen Referenz wie einem RFC oder einer Norm, also von etwas, das aus einer ganz anderen Quelle stammt – oder von einer zweiten KI, die du adversariell ansetzt, als Angreifer, der Gegenbeispiele jagt und nicht als Echo nickt. Dass die Antwort auf unsere angeblich nagelneue Frage seit 1986 in einer Schublade liegt, sagt mehr über unser Gedächtnis als über die KI.

Das Spezifikationsproblem bleibt

Die Kosten des Beweisens sinken, der Wert einer harten Garantie steigt in einer Welt, in der niemand mehr jede Zeile liest, und das Spezifikationsproblem bleibt so schwer, wie es immer war, weil es nie am Werkzeug lag. Die Wurzel der ganzen Kette muss am Ende in etwas Nicht-Generiertem sitzen, in einem Menschen oder einer externen Autorität, sonst dreht sich das System im Kreis und bestätigt nur sich selbst. Das größte neue Risiko ist kulturell, das automatisierte Selbstvertrauen: interne Konsistenz mit Korrektheit zu verwechseln, weil das grüne Häkchen die Frage erstickt, ob das Bewiesene überhaupt das Richtige war.

Wo Verifikation ihren Preis verdient

Verifikation lohnt sich da, wo ein Fehler katastrophal ist und Testen ihn nicht zuverlässig findet, und diese Linie liegt heute genau da, wo sie schon vor der KI lag. Es sind sehr spezielle Ecken: Nebenläufigkeit, wo der eine Bug nur bei der einen Verschränkung von Threads auftritt, die dein Test nie trifft; Crash- und Recovery-Sicherheit, wo dein Speicher nach einem Stromausfall mitten in einer Operation nicht still korrumpieren darf; Sicherheits- und Konsensprotokolle, wo ein Angreifer aktiv nach der Lücke sucht. Die Vorzeigefälle sind ein Router-Protokoll oder ein crashsicherer Speicher wie bei Goose und Perennial, maschinengeprüft bis es weh tut, und eben nicht die CRUD-App, die Formulare in eine Datenbank schreibt. Für dein Web-Backend hat sich der Aufwand vorher nicht gelohnt und lohnt sich auch jetzt nicht; was die KI dort bringt, sind billigere gute Tests, mehr nicht. Die Linie liegt, wo sie immer lag. Neu ist allein, dass ihre teure Seite auf einmal erreichbar wird für Teams, die sich die Annotationsarbeit früher schlicht nicht leisten konnten.

Ich habe es selbst ausprobiert

Ich habe Design by Contract in meinen Go-Projekten eingeführt, über dbc4go. Design by Contract ist übrigens auch nicht neu – Bertrand Meyer hat es mit Eiffel Mitte der 80er gebaut, etwa zu der Zeit, als ich gerade von Z80-Assembler auf C umstieg und einen Vertrag noch für etwas hielt, das man mit Anwälten schließt und nicht mit Compilern. Vierzig Jahre später annotiert mir die KI den Code mit genau diesen Verträgen, und der annotierte Code läuft als finales Gate neben den Tests. Die Geschwindigkeit bleibt, weil kein SMT-Solver mahlt und kein Build sich in die Länge zieht, und der Rigor steigt trotzdem spürbar, weil die Absicht jetzt an zwei Stellen steht und jede Abweichung zwischen den beiden sofort auffällt, ungefähr so, wie die doppelte Buchführung dem Kaufmann den Fehler zeigt, lange bevor die Bilanz lügt.

Ein Beweis ist das nicht. Es ist der billige Teil der Unabhängigkeit, die kleine Abstraktionslücke zwischen Code und Vertrag, und Autor und KI bleiben dieselbe Quelle – schreibe ich den Vertrag im selben Atemzug wie den Code, lande ich genau in der Falle von oben. Mal sehen, wie es sich auf Dauer bewährt. Ein Experiment, kein Rezept.

Steig nur so hoch, wie das System es verdient

Die Debatte vergiftet ein Entweder-oder: voller maschinengeprüfter Beweis oder eben gar nichts. Bau dir stattdessen eine Leiter und steig nur so hoch, wie ein Stück Code es verdient. Unten stehen dieselben Verträge wie bei mir, als Kommentare im Code, zur Laufzeit geprüft, ohne SMT und ohne langsamen Build, breit ausrollbar über die ganze Codebase, und sie geben dir lebende Dokumentation, die nicht veraltet weil sie geprüft wird, und ein Fail-fast statt einer stillen Korruption, die dir erst drei Wochen später um die Ohren fliegt. Eine Stufe höher nimmst du genau dieselben Verträge als Test-Orakel und lässt Fuzzing und Property-Testing dagegen laufen, und hier kommt die Unabhängigkeit zurück, die ein zweites Modell nie liefern konnte, denn sie stammt diesmal aus der Eingabequelle, aus den zufälligen, gemeinen, ungedachten Eingaben, die der Fuzzer gegen deinen Vertrag wirft. Ganz oben, für die kritischen fünf Prozent und keinen Deut mehr, steht die volle statische Verifikation mit Gobra oder Goose und Perennial, sound, aber teuer und hungrig nach Spezialwissen. Über alle drei Stufen bleibt das Vertragsvokabular dasselbe, dieselbe alte Hoare-Logik, und deshalb fällt die teure Arbeit, zu entscheiden, was überhaupt zugesichert wird, nur einmal an und wandert mit nach oben, sobald ein Stück Code es verdient. Du fängst klein an, ohne dich einzumauern.

Der Preis, den keiner nennt: Menschen

Über den teuersten Posten redet bei all dem fast niemand, und es sind die Leute. Die unteren Stufen brauchen kein neues Spezialistenteam, da reichen gute Ingenieure, etwas Disziplin und die KI, die die Fleißarbeit übernimmt. Die oberste Stufe braucht rares Wissen, Separationslogik und Beweisassistenten und Leute, die man nicht eben so im Markt findet, und das spricht eher für eine Partnerschaft als für den Versuch, sich das intern aufzubauen, es sei denn, Verifikation ist euer Kerngeschäft. Das größte Risiko ist am Ende kulturell: Verifikation als Beruhigungstheater, in dem die Häkchen leuchten, während niemand die Spezifikationen je ernsthaft gelesen hat.

Wer die Spec gemeint haben muss

Das „jetzt endlich" stimmt, für das Beweisen. Beim Verstehen bleibt alles beim Alten: Wer eine Spec schreiben und ernsthaft prüfen kann, konnte das vorher auch, und wem das fehlt, dem hilft auch das billigste Werkzeug nicht. Nach dem Beweis vertraust du immer noch jemandem, dem Spec-Text, der Soundness von Gobra, der Übersetzung dazwischen, und irgendwer muss diese Spec geschrieben und im Kopf gehabt haben, sonst hängt die ganze Kette in der Luft.

Deine Arbeit als Entscheider bleibt dieselbe: für jedes System die richtige Stufe wählen, und jedem grünen Häkchen misstrauen, hinter dem niemand die Absicht je besessen hat. Die KI beweist dir bald fast alles. Was sie dir nie abnimmt: die Entscheidung, was überhaupt wahr sein soll. Die triffst weiter du.