Anthropic und das Verifikations-Startup Theorem haben bestehende Fuzz-Tests aus Googles OSS-Fuzz-Projekt mithilfe des KI-Modells Claude in mathematische Spezifikationen übersetzt. Laut einem Forschungspost des Frontier Red Teams von Anthropic erzeugte das System am 22. Oktober 2026 maschinell überprüfte Beweise für die Absturzfreiheit von 239 Test-Einstiegspunkten in 123 Open-Source-Bibliotheken auf RISC-V-Assembly-Ebene.
Umfang und Tempo
Nach Angaben der beiden Partner entstanden im Rahmen des Projekts rund 180 Millionen Zeilen Beweiscode im formalen System Rocq. Ein typischer Beweis umfasst etwa 600.000 Zeilen, während die analysierten Binärdateien im Median rund 18.000 RISC-V-Befehle zählen. Die Validierung übernahm das Beweisprüfungswerkzeug Rocq. Anthropic und Theorem geben an, die Beweise in wenigen Wochen erstellt zu haben, und stellen dem den historischen Aufwand von 20 Personenjahren gegenüber, der für die Verifikation des seL4-Betriebssystemkerns nötig war.
Gefundene Fehler
Während des Prozesses entdeckte und reparierte Claude laut den Angaben hunderte Programmierfehler, die zuvor selbst von Billionen automatisierter Testdurchläufe unbemerkt geblieben waren. Genannt werden unter anderem ein Pufferüberlauf durch einen Zähler-Unterlauf in einem Dekomprimierer, der nur bei einem seltenen Speicherlayout von rund 20 Megabyte auftrat, sowie ein unzulässiger Lesezugriff außerhalb der Speichergrenzen in einem Bild-Dekodierer bei einer Eingabegröße von 64 Megabyte. Übliche Fuzz-Tests prüfen meist nur Eingabegrößen bis etwa 1 Megabyte. Zudem wurde die Sicherheitslücke CVE-2026-56132 in der Bibliothek libexpat wiederentdeckt, ergänzt um einen Logikfehler, der über zehn Jahre verborgen geblieben war. Bei einem PDF-Betrachter fand Claude innerhalb einer einzigen Woche so viele Sicherheitsmängel, wie Entwickler sonst in einem ganzen Jahr verzeichnen.
Grenzen der Aussagekraft
Anthropic und Theorem weisen ausdrücklich auf methodische Grenzen hin. Die Beweise gelten nur für einsträngig ausgeführte, statisch verknüpfte RISC-V-Programme mit der musl-C-Bibliothek unter einer modellierten Linux-Umgebung, bei einem festen Speicherbudget und Eingaben unter 64 Megabyte. Für gängige x86- oder ARM-Architekturen sowie die weit verbreitete Standardbibliothek glibc greifen die Resultate nicht. Vollständige Fehlerfreiheit wird nicht garantiert; Restunsicherheiten bleiben in der Semantikmodellierung von RISC-V und Linux, in den Theoremaussagen, im Rocq-Prüfprogramm und in den Spezifikationen für AddressSanitizer.
Hintergrund
Die Rechenintensität bleibt hoch: Anthropic bezifferte die Kosten für einen einzelnen Beweis auf hunderte Millionen Token. Laut den Angaben bewältigte das Modell Opus 5.5 die Hälfte von 36 Testaufgaben mit rund 40 Prozent weniger Token als Opus 5. Der Einsatz spezialisierter Agenten in geteilten Arbeitsbereichen reduzierte den Token-Verbrauch im Vergleich zu Einzelläufen um 17 Prozent. Anthropic stellte am 22. Oktober 2026 die RISC-V- und Betriebssystemsemantik sowie Beweise für 60 Einstiegspunkte in 25 Bibliotheken in einem öffentlichen Repository bereit. Theorem bietet den Dienst OSS Verify für Open-Source-Software an und strebt die formale Überprüfung des Paketmanagers Nix samt glibc, OpenSSL und cURL an.
Einordnung
Für Unternehmen mit Abhängigkeiten von Open-Source-Bibliotheken könnte die Methode perspektivisch relevant werden, etwa wenn sich formale Nachweise auf weitere Architekturen und Standardbibliotheken ausdehnen lassen. Offen bleibt, wie belastbar die Ergebnisse außerhalb der untersuchten Bedingungen sind und wer die Kosten der Verifikation trägt.
Quellen
Redaktionell verantwortet von Ideal Syka. Quellen und Arbeitsweise: Redaktion & Methode. Hinweise und Korrekturen: ai@i6eal.de.
