Das Frontier Red Team von Anthropic hat am 22. Oktober eine Studie veröffentlicht, in der Claude für 239 Einstiegspunkte in 123 Open-Source-Bibliotheken formale Beweise erstellt hat: Solange die Eingabe kleiner als 64 MB ist, stürzen diese Programme nicht ab. Die Beweise setzen direkt auf den kompilierten RISC-V-Programmdateien auf; Partner ist Theorem, ein Anbieter von Werkzeugen für formale Verifikation. Anthropic zufolge ist es das erste Mal, dass KI formale Verifikation auf der Assembler-Ebene von Produktivsoftware in großem Maßstab betreibt.
Alle Bibliotheken stammen aus Googles Projekt OSS-Fuzz, also jener Basiskomponenten, die dauerhaft auf der Fuzzing-Plattform laufen; Kompression, Bilddekodierung und HTTP-Parsing sind darunter. Das gesamte Vorhaben dauerte einige Wochen.
Fuzz-Tests werden zu Theoremen
Das Vorgehen hat drei Schritte. Erstens schrieb das Team die vorhandene Fuzz-Testsuite jeder Bibliothek in eine formale Spezifikation um, sinngemäß: „Dieser Testcode stürzt bei beliebiger Eingabe nicht ab.“ Die Spezifikation baut auf den von Theorem bereitgestellten Modellen der RISC-V-Befehlssemantik und der Linux-Prozesssemantik auf.
Im zweiten Schritt schreibt Claude den Beweis, den der Beweisprüfer Rocq anschließend Schritt für Schritt kontrolliert.
„Claude writes the proof; the Rocq kernel checks it against the specification.“ (Claude schreibt den Beweis, der Rocq-Kern prüft ihn gegen die Spezifikation.)
Der dritte Schritt betrifft den Fall, dass ein Beweis nicht gelingt. Bleibt ein Beweis stecken, steckt oft tatsächlich ein Fehler im Code; dann ändert Claude den Code selbst, die Spezifikation wird neu erzeugt, und es geht weiter. Das Team räumt ein, dass hier „Reward Hacking“ naheliegt: Das Modell könnte das Programm wahllos verändern, nur damit der Beweis durchgeht. Deshalb wurden Patches mit einer Strafe belegt; verlangt wird der Nachweis, welchen Eingabebereich ein Patch betrifft, und jeder Patch wird protokolliert und manuell geprüft.
Ein typischer Beweis umfasst rund 600.000 Zeilen. Vertrauen muss man am Ende nur noch den Semantikmodellen für RISC-V und Linux, der Formulierung des Theorems selbst und dem Rocq-Prüfer.
Fehler, die beim Beweisen auftauchten
Beim Beweisen wurden mehrere hundert Fehler gefunden und behoben, darunter einige, die sich per Fuzzing kaum aufspüren lassen. Der Beitrag nennt mehrere Beispiele: ein Zähler-Unterlauf in einem Dekompressor, der nur bei bestimmten Eingaben von etwa 20 MB auftritt; ein Lesezugriff außerhalb der Grenzen in einem Bilddekoder, für den 64 MB Eingabe und mehr als 2 GB Arbeitsspeicher nötig sind; ein weiterer Lesezugriff außerhalb der Grenzen, der verlangt, dass zwei Handles in bestimmter Reihenfolge auf dieselbe Datei zugreifen. Auch die libexpat-Schwachstelle CVE-2026-56132 wurde dabei erneut entdeckt.
Bei cpp-httplib kam eine zusätzliche Hürde hinzu: Die Rekursion beim Zerstören eines std::set kann zu einem Stapelüberlauf führen. Um das auszuschließen, bewies das Team auf Maschinencode-Ebene, dass der Balancierungsalgorithmus des Rot-Schwarz-Baums in libc++ die Baumtiefe logarithmisch begrenzt.
Dieselbe Studie enthält außerdem einige Nebenexperimente. Claude schrieb in Rust eine Teilmenge von Python und bewies mit Verus, dass sie der CPython-Semantik entspricht; auf 1,7 Millionen Zufallsprogrammen stimmte das Verhalten in 99,95 % der Fälle mit CPython überein. Außerdem erzeugte Claude selbst eine x86-Befehlssemantik, mit der sich per Einzelschritt-Ausführung ein Ubuntu-Userspace starten lässt, und fand dabei nebenbei mehrere hundert Fehler in der offiziellen Referenzdokumentation.
Zum Vergleich: seL4
Formale Verifikation ist in der Industrie nichts Neues, die Hürde war immer der Personalaufwand. Als Beispiel wird gern der Mikrokernel seL4 angeführt: rund zehntausend Zeilen C-Code, für die der Beweisaufwand damals üblicherweise mit etwa zwanzig Personenjahren beziffert wird. Auch der Compiler CompCert folgt einem ähnlichen Weg und wurde von einem kleinen Team über Jahre hinweg geschliffen. Gemeinsam ist diesen Projekten: wenige Objekte, lange Laufzeit, viele Experten.
Anthropic kommt diesmal auf 123 Bibliotheken in wenigen Wochen; grob verglichen hat die Kostenstruktur pro Arbeitseinheit eine andere Gestalt angenommen, der Mensch zieht sich vom Schreiben der Beweise auf das Festlegen von Spezifikationen und das Prüfen von Patches zurück. Der Preis wird in Token bezahlt: Laut dem Beitrag kann ein vollständiger Beweis mehrere hundert Millionen Token verbrauchen. Bei den 36 kleinen Aufgaben bekam jeder Agent pro Aufgabe drei Versuche mit je 5 Millionen Token Budget; durften die Agenten Beweise voneinander wiederverwenden, sank der Tokenbedarf noch einmal um 17 %.
Auch die Stärke der Garantien liegt auf unterschiedlichen Ebenen. seL4 beweist funktionale Korrektheit, hier wird nur „kein Absturz“ bewiesen, ein deutlich engerer Umfang.
Lücken jenseits des Beweises
Die Einschränkungen, die Anthropic selbst aufführt, sind recht konkret. Die Beweise beziehen sich auf einthreadige, statisch gelinkte RISC-V-Binärdateien mit musl libc, während die meisten Nutzer tatsächlich Versionen für x86 oder ARM mit dynamisch gelinktem glibc einsetzen. AddressSanitizer selbst findet nicht alle Speichersicherheitsfehler, einzelne Einstiegspunkte sind nicht abgedeckt, und Speicherbeschädigungen durch falsche Nutzung der Bibliothek auf Aufruferseite liegen ebenfalls außerhalb des Beweises.
„Formally verified“ does not mean „bug-free.“ („Formal verifiziert“ heißt nicht „fehlerfrei“.)
Die Abweichung zwischen Spezifikation und realer Maschine ist die Stelle, an der dieser Weg am ehesten schiefgeht. Auch Rocq und die Semantikmodelle selbst müssen gehärtet werden, was der Beitrag als „keine Kleinigkeit“ bezeichnet. Das Team geht davon aus, dass formale Verifikation zu einem Standardbestandteil sicherer Softwareentwicklung wird; wann diese Beweise gängige Einsatzumgebungen wie x86 und glibc abdecken, nennt der Beitrag nicht.
Quellen: Forschungsbeitrag des Frontier Red Team von Anthropic, CocoLoop; die Forschungsseite von Anthropic diente zur Prüfung von Bibliotheksanzahl, Einstiegspunkten, Beweiszeilen und der Vergleichsgrundlage beim Token-Verbrauch.