KI macht Formale Verifikation wieder wirtschaftlich

Der starke Anstieg KI-generierter Software rückt eine seit über fünf Jahrzehnten bekannte Technik zurück ins Zentrum der Technologiebranche: die formale Verifikation. Google-Chef Sundar Pichai berichtete zuletzt von 75 Prozent KI-generiertem neuem Code, bei Anthropic soll es intern über 80 Prozent sein. Gleichzeitig stellte die Prüfplattform CodeRabbit bei KI-beteiligten Pull Requests in 470 Open-Source-Projekten 1,7-mal mehr Fehler fest. Da Menschen KI-Erzeugnisse nicht mehr im selben Tempo prüfen können, wächst das Interesse an mathematischer Absicherung. Formale Verifikation beschreibt Anforderungen als präzise mathematische Eigenschaften und beweist, dass ein Programm diese für alle Eingaben erfüllt. Werkzeuge wie Lean, Rocq und Isabelle prüfen die Beweise maschinell. Ihre Wurzeln reichen von Automath und Hoare-Logik bis zu Coq. Bisher war der Ansatz teuer und auf Nischen begrenzt, etwa Mikrokernel seL4, Chipentwicklung oder Krypto-Bibliotheken; Apple, Amazon und Boeing setzen verifizierte Software für sicherheitskritische Komponenten ein. Der Stanford-Doktorand Chuyue Sun berichtete im August, dass ein KI-System die Verifikation einer Krypto-Bibliothek nach einer manuellen Vorleistung in 11,4 Stunden und für rund 467 US-Dollar vervollständigte. Im industriellen Maßstab zeigt sich die neue Wirtschaftlichkeit. Anthropic und das Start-up Theorem nahmen 123 von Google gepflegte Bibliotheken, übertrugen Testfälle in Spezifikationen und ließen Claude maschinelle Beweise erstellen; dabei entstanden etwa 180 Millionen Zeilen Nachweiscode, und mehrere Hundert Schwachstellen wurden behoben. Axiom Math formalisierte mit KI-Agenten in 24 Tagen einen 43,1 Millionen Zeilen langen Beweis der Klassifikation endlicher einfacher Gruppen und fand dabei 34 Fehler in historischen Veröffentlichungen. Der Markt zieht Kapital an. Axiom, Harmonic, UndTruth und Pramaana Labs haben zusammen mehr als 650 Millionen US-Dollar eingesammelt. Harmonics Beweiser Aristotle, zuvor als IMO-Gold-Level beschrieben, prüft seit Oktober C-Programme und Chips. UndTruth erhielt im Oktober 70 Millionen US-Dollar Seed-Finanzierung und will mit Lean eine breitere Code-Verifikation automatisieren. Experten betonen jedoch Grenzen. Verifikation beweist nur Übereinstimmung mit Spezifikationen; irrtümliche Anforderungen oder KI-generierte Axiome können falsche Sicherheit erzeugen. Ethereum-Gründer Vitalik Buterin sieht den Ansatz nicht als Allheilmittel, hält ihn aber für eine zentrale Abwehr gegen KI-gestützte Angriffe. Auch wenn Proofcraft eine gestiegene Nachfrage meldet, bleibt unklar, wer die Standards setzt. Entscheidend sei nicht die Beweisschnelligkeit allein, sondern ob die Prüfung transparent und unabhängig bleibt.