Anthropic berichtete am 22. Oktober 2026 über ein gemeinsames Projekt mit Theorem, in dem Claude Beweise für 239 Fuzz-Test-Einstiegspunkte aus 123 Google-OSS-Fuzz-Bibliotheken erzeugte. Der Rocq-Kernel prüfte die Beweise. Die behauptete Absturzfreiheit gilt für Eingaben unter 64 MB und ein festgelegtes Modell aus statischem RISC-V-Programm, Linux und begrenztem Speicher.
Wie aus Fuzz-Tests maschinengeprüfte Beweise werden
Fuzzing ist ein Testverfahren, bei dem ein Programm mit vielen automatisch erzeugten Eingaben ausgeführt wird. Anthropic und Theorem überführten bestehende Fuzz-Tests in formale Spezifikationen für kompilierte RISC-V-Programme. Claude erzeugte den Beweiscode; der Rocq-Kernel prüfte, ob er aus der jeweiligen Spezifikation folgt. Theorem steuerte die RISC-V- und Linux-Prozesssemantik bei, also die Regeln, nach denen das Modell die Ausführung abbildet.
Was die 239 geprüften Einstiegspunkte abdecken
Anthropic berichtet, dass die Beweise für jeden geprüften Einstiegspunkt Abstürze bei allen Eingaben unter 64 MB ausschließen, sofern die festgelegten Modellbedingungen gelten. Dazu gehörten ein einzelner Thread, ein statisches RISC-V-Programm, ein festes Speicherbudget und das Linux-Modell. Die mittlere Länge der geprüften Binärprogramme betrug laut Anthropic 18.000 RISC-V-Befehle.
Die Aussage bezieht sich auf ausgewählte Einstiegspunkte und die formalisierte Absturz-Eigenschaft. Anthropic zufolge wurden nicht alle Einstiegspunkte der Bibliotheken geprüft. Der Beweis deckt daher weder automatisch jede Funktion einer Bibliothek noch jedes Verhalten eines darauf aufbauenden Programms ab.
Welche Fehler während der Beweisversuche auffielen
Anthropic nennt unter anderem einen seltenen Fehler in einem Dekomprimierer: Ein Zähler lief unter, was bei einer Eingabe von ungefähr 20 MB zu einem Schreibzugriff außerhalb des vorgesehenen Speicherbereichs führte. Bei einem Bilddecoder erforderte ein Lesezugriff außerhalb dieses Bereichs eine 64-MB-Eingabe und mehr als 2 GB Arbeitsspeicher. Anthropic berichtet außerdem von einem Fehler in libexpat, der als CVE-2026-56132 bezeichnet wird und bei tief verschachtelten Eingaben wiederentdeckt wurde.
Laut Anthropic behob Claude während der Beweisversuche entdeckte Fehler und erzeugte anschließend Spezifikationen für den jeweils geänderten Code. Anthropic zufolge wurden Änderungen protokolliert und geprüft; außerdem verlangte das Team Belege dafür, welche Eingaben sich durch einen Patch änderten, und bewertete Patches im Verfahren mit Abschlägen.
Wo die Garantie ihre Grenzen hat
Ein geprüfter Beweis zeigt, dass ein Programm die festgelegte Eigenschaft im verwendeten formalen Modell erfüllt. Er prüft nicht, ob die Spezifikation jedes Verhalten erfasst, das Nutzer von der Software erwarten, oder ob das Modell alle realen Maschinenbedingungen abbildet. Anthropic beschreibt die Hauptversuche als statische, einsträngige RISC-V-Programme unter Linux; reale Anwendungen können andere Prozessorarchitekturen und dynamische Verknüpfung verwenden.
Auch weitere Teile des Softwareeinsatzes liegen außerhalb dieser Aussage: Ein Aufrufer kann eine Bibliothek fehlerhaft verwenden, und nicht geprüfter Code erhält durch den Beweis für einen ausgewählten Einstiegspunkt keine entsprechende Garantie. Anthropic weist zudem darauf hin, dass AddressSanitizer, ein Werkzeug zum Erkennen bestimmter Speicherfehler während der Programmausführung, nicht alle Speicherfehler findet.
Was die Beweisgrößen und der Python-Fall ergänzen
Anthropics Anhang unterscheidet rund eine Milliarde erzeugte Rocq-Zeilen aus Beweisversuchen von etwa 180 Millionen Zeilen, die in erfolgreich geprüften Beweisen enthalten waren. Ein typischer fertiger Beweis umfasste demnach ungefähr 600.000 Zeilen in rund 1.400 Dateien. Die Prüfung eines Beweises dauerte laut Anhang zwischen 30 Minuten und mehreren Stunden CPU-Zeit.
In einer separaten Fallstudie ließ Anthropic mit Verus alle 17 Stufen eines in Rust geschriebenen Python-Interpreters gegen die formale Semantik des Projekts prüfen. Der Vergleich mit CPython war dagegen empirisch: Bei mehr als 1,7 Millionen überwiegend zufällig erzeugten Programmen stimmte das Verhalten laut Anthropic in 99,95 Prozent der Fälle überein. Dieser Messwert beschreibt die getesteten Programme; der formale Beweis bezog sich auf die definierte Semantik.
