Der Beweis, den die Maschine selbst prüft: Warum formale Verifikation plötzlich bezahlbar wird

Das eigentlich Bemerkenswerte stand nicht in der Schlagzeile

Am 10. August teilte Anthropic mit, ein unveröffentlichtes Claude-Modell habe eine Schranke rund um die Riemann-Hypothese verbessert — von 41,6 auf 67,2 Prozent. Die Schlagzeilen konzentrierten sich erwartbar auf das Millionen-Dollar-Problem und darauf, dass eine Maschine dort weiterkam, wo Menschen 150 Jahre lang zäh gerungen hatten.

Interessanter für alle, die keine Zahlentheorie betreiben, ist ein Detail am Rand: Das Ergebnis wurde in Lean formalisiert, einem sogenannten Beweisassistenten. Diese Formalisierung besteht ein Standard-Prüfwerkzeug. Im Klartext heißt das: Man muss dem Modell nicht glauben. Man muss auch den beiden Anthropic-Mathematikern nicht glauben, die das Ergebnis gegengelesen haben. Ein Programm hat jeden einzelnen Schritt mechanisch nachgerechnet.

Das ist eine ungewöhnliche Situation. Ein System, das nachweislich halluziniert, das 650 Ideen durchprobierte und dabei in 60 parallelen Teilprozessen 31 Millionen Token verbrauchte, liefert am Ende ein Ergebnis, dessen Korrektheit nicht mehr von seiner Glaubwürdigkeit abhängt. Die Prüfung ist von der Erzeugung entkoppelt.

Genau darin liegt die Relevanz für Unternehmen — und sie hat mit Zahlentheorie nichts zu tun.

Was ein Beweisassistent tut, in einem Absatz

Ein Beweisassistent wie Lean ist am ehesten mit einem extrem pedantischen Compiler zu vergleichen. Ein normaler Compiler prüft, ob Ihr Code syntaktisch zulässig ist und ob die Typen zusammenpassen. Ein Beweisassistent prüft, ob eine Behauptung aus den angegebenen Voraussetzungen folgt — lückenlos, bis hinunter auf die Axiome. Er akzeptiert kein „das ist offensichtlich“ und kein „analog zu oben“. Wer einen Schritt auslässt, bekommt einen Fehler.

Übertragen auf Software heißt das: Statt zu testen, ob ein Programm bei 500 ausgewählten Eingaben das Richtige tut, beweist man, dass es bei allen möglichen Eingaben das Richtige tut. Tests finden Fehler. Beweise schließen sie aus.

Der Haken war immer der Preis.

Warum das dreißig Jahre lang unbezahlbar war

Das kanonische Beispiel ist seL4, ein formal verifizierter Betriebssystem-Mikrokernel. Die Beweise reichen von der abstrakten Spezifikation bis hinunter zum Maschinencode und schließen Eigenschaften wie funktionale Korrektheit und die Abwesenheit von Informationslecks ein. Es ist eine der beeindruckendsten Ingenieursleistungen der Informatik.

Es ist auch eine Abschreckung. Nach den Veröffentlichungen des Projekts kostete die ursprüngliche Verifikation rund zwölf Personenjahre für etwa 8.500 Zeilen Quellcode — überschlägig einige hundert Dollar pro Zeile. Über die Jahre und alle Architekturen hinweg summierte das Projekt mehr als zwanzig Personenjahre.

Bei diesen Zahlen ist die betriebswirtschaftliche Rechnung schnell fertig. Formale Verifikation lohnte sich für Kernreaktoren, Flugsteuerungen, Herzschrittmacher und Kryptografie-Bibliotheken. Für Ihr Abrechnungsmodul lohnte sie sich nicht — nicht, weil Korrektheit dort unwichtig wäre, sondern weil ein Beweis mehr kostete als der Schaden, den er verhindert.

Der teure Teil war dabei nie der Prüfschritt. Prüfen ist billig und läuft automatisch. Teuer war das Schreiben der Beweise: die stumpfe, hochqualifizierte Handarbeit, jede Lücke zu schließen, die ein Mensch überspringen würde.

Und genau diese Handarbeit ist das, was Sprachmodelle inzwischen leidlich beherrschen.

Was sich 2026 verschoben hat

Die Bewegung der letzten achtzehn Monate lässt sich in einem Satz zusammenfassen: Die Erzeugung formaler Beweise wurde automatisiert, während die Prüfung schon immer automatisch war.

Ein Team formalisierte nach eigener Darstellung 130.000 Zeilen formaler Topologie in zwei Wochen — eine Arbeitsmenge, die klassisch als Mehrjahresprojekt gegolten hätte. Einzelne dokumentierte Formalisierungen von Fachpublikationen liegen bei Rechenkosten im niedrigen dreistelligen Dollarbereich. Mistral veröffentlichte am 16. März 2026 mit Leanstral ein quelloffenes Modell (Apache 2.0) speziell für Lean-4-Beweisführung, ausdrücklich mit dem Ziel, Coding-Agenten ihre Implementierungen gegen strenge Spezifikationen beweisen zu lassen. Das System Aristotle der Firma Harmonic lieferte formal verifizierte Lösungen für fünf der sechs Aufgaben der Internationalen Mathematik-Olympiade 2025 — auf Goldmedaillen-Niveau und vollständig in Lean maschinell geprüft, ohne menschliche Nachkontrolle.

Wichtig ist dabei die Asymmetrie, die das alles trägt. Ein Sprachmodell, das Beweise vorschlägt, darf sich irren, so oft es will. Der Prüfer sortiert die Fehlversuche aus. Es gibt in dieser Pipeline keinen Weg, auf dem eine Halluzination als Ergebnis durchrutscht. Das ist der seltene Fall, in dem die bekannteste Schwäche der Technologie strukturell folgenlos bleibt.

Wir haben an dieser Stelle im Juni über das Verifikationsproblem geschrieben: Erzeugung wird billig, Prüfung bleibt teuer, und der Engpass wandert zum Menschen, der den Output kontrollieren muss. Was hier passiert, ist die Auflösung genau dieser Asymmetrie — allerdings nur dort, wo sich das Gewünschte präzise hinschreiben lässt.

Wo es produktiv läuft

Das ist keine Zukunftsmusik mehr, aber es ist auch nicht überall.

AWS verifiziert Cedar, seine Sprache für Zugriffsregeln, mit Lean. Das ist ein gut gewähltes Ziel: Autorisierungslogik ist sicherheitskritisch, kompakt und präzise beschreibbar. Die Frage „Kann Nutzer A jemals auf Ressource B zugreifen?“ hat eine mathematisch saubere Form.

Microsoft Research verifiziert kryptografische Produktionsalgorithmen in SymCrypt — der Bibliothek hinter Windows, Azure und Xbox — über die Aeneas-Toolchain in Lean. Die Konstruktion ist doppelt abgesichert: Rust schließt ganze Klassen von Speicherfehlern aus, die Lean-Beweise zeigen die funktionale Korrektheit gegenüber den aus den Standards abgeleiteten Spezifikationen. Veröffentlicht werden Code, Spezifikationen und Beweise zunächst für SHA-3 und ML-KEM. Auch hier: enge, klar spezifizierbare Domäne, katastrophale Folgen bei Fehlern.

Das Muster ist erkennbar. Formale Verifikation setzt sich dort durch, wo die Spezifikation kürzer ist als die Implementierung — Parser, Kryptografie, Zugriffskontrolle, Compiler, Konsensprotokolle, Finanzarithmetik. Sie setzt sich nicht durch, wo die Anforderung selbst unscharf ist. Für „der Checkout-Flow soll sich gut anfühlen“ gibt es keinen Beweis, und es wird auch keinen geben.

Der Engpass wandert — und zwar dorthin, wo er wehtut

Damit verschiebt sich die eigentliche Arbeit. Je schneller KI Code erzeugt, desto mehr wird die Spezifikation zur knappen Ressource. Nicht mehr das Schreiben ist der Flaschenhals, sondern das präzise Festlegen dessen, was gelten soll — und genau das lässt sich nicht an das Modell delegieren, denn es ist die Frage, was das Unternehmen überhaupt will.

Das ist für die meisten Organisationen eine unangenehme Nachricht, denn es ist genau die Disziplin, die am wenigsten gepflegt wurde. Anforderungen existieren als Tickets, Slack-Fäden und mündliche Absprachen. Man kann einem Modell nicht beweisen lassen, dass ein Programm tut, was gemeint war, wenn niemand aufgeschrieben hat, was gemeint war.

Die Forschung hat das Problem inzwischen sauber benannt: Ein Benchmark wie Verus-SpecGym misst nicht mehr, ob Modelle Code schreiben können, sondern ob sie aus informellen Beschreibungen brauchbare formale Spezifikationen ableiten. Dass es diesen Benchmark gibt, ist selbst die Aussage.

Was das praktisch bedeutet

Für die allermeisten Teams lautet die Konsequenz nicht „führt Lean ein“. Sie lautet: Auf der Leiter der maschinell prüfbaren Zusicherungen steht Ihr Team wahrscheinlich zwei Sprossen tiefer, als es müsste — und die oberen Sprossen sind gerade billiger geworden.

Die Leiter, von unten:

1. Typen. Die billigste Form maschineller Prüfung. Ein Zustand, den der Typ nicht zulässt, muss nie getestet werden. Wer any verteilt, verschenkt Beweiskraft, die er bereits bezahlt hat.
2. Eigenschaftsbasierte Tests. Statt fünf Beispiele zu prüfen, formulieren Sie eine Regel („jede Buchung und ihre Stornierung ergeben null“) und lassen das Werkzeug tausende Fälle suchen, die sie brechen. Der Aufwand ist gering, und es ist die Stufe, auf der KI-Assistenz heute am unmittelbarsten hilft.
3. Ausführbare Verträge und Invarianten. Vor- und Nachbedingungen, Datenbank-Constraints, Zustandsautomaten. Was das System niemals tun darf, gehört an eine Stelle, die es erzwingt — nicht in ein Confluence-Dokument.
4. Formale Verifikation. Für den kleinen, teuren Kern: Preisberechnung, Rechteprüfung, Protokoll-Handling.

Der gemeinsame Nenner: Wer KI-geschriebenen Code ausliefert, braucht Zusicherungen, die eine Maschine prüfen kann. Denn die menschliche Prüfkapazität skaliert nicht mit, und ein Review, das nur noch überflogen wird, ist ein Ritual, kein Kontrollpunkt.

Die Riemann-Meldung ist deshalb weniger eine Mathematik-Nachricht als ein Vorführmodell. Sie zeigt eine Arbeitsteilung, die trägt: Die Maschine darf raten, so wild sie will — solange am Ende etwas steht, das sich mechanisch nachrechnen lässt. Übertragen auf Ihre Codebasis ist die entscheidende Frage nicht, wie viel Ihre Agenten schreiben. Sie lautet, wie viel von dem, was sie schreiben, überhaupt maschinell prüfbar ist.