Anthropic behauptet, Claude habe bewiesen, dass 123 Open-Source-Bibliotheken nicht abstürzen können
Anthropic und Theorem nutzten Claude, um 180 Millionen Zeilen maschinell geprüfter Beweise zu schreiben, die zeigen, dass Fuzz-getesteter Code in 123 Open-Source-Bibliotheken nicht abstürzen kann, und entdeckten dabei lange verborgene Fehler.
Anthropic behauptet, Claude habe mathematisch bewiesen, dass der Fuzz-getestete Code in 123 Open-Source-Bibliotheken bei keiner Eingabe unter 64 MB abstürzen könne, und dabei seien Fehler entdeckt worden, die jahrelange Tests übersehen hatten.
Das Werk, herausgegeben von Anthropic am 22. Oktober Mit dem Start-up Theorem, das sich auf formale Verifikation spezialisiert hat, werden 239 Einstiegspunkte aus Googles OSS-Fuzz-Projekt abgedeckt. Anthropic bezeichnet dies als den ersten groß angelegten Versuch, KI zur formalen Verifikation von Produktionssoftware auf Assembler-Code-Ebene einzusetzen.
Von Tests zu Beweisen
Beim Fuzzing werden unzählige zufällige Eingaben an ein Programm gesendet, um Fehlerquellen zu finden. Dabei können jedoch nie alle Eingaben getestet werden. Anthropic wandelte jeden bestehenden Fuzz-Test in eine formale Regel um: “Dieser Test führt niemals zu einem Absturz.” Claude bewies, dass diese Regel für alle Eingaben unter 64 MB gilt.
Die Beweise basieren auf kompiliertem RISC-V-Maschinencode, nicht auf Quellcode. Innerhalb weniger Wochen schrieb Claude im Beweisassistenten Rocq etwa 180 Millionen Zeilen Beweise, was bei einem typischen Programm etwa 600.000 Zeilen entspricht. Kein Mensch muss sie lesen; der Rocq-Prüfer bestätigt jeden einzelnen automatisch.
Fehlertests verpasst
Immer wenn ein Beweis fehlschlug, hatte Claude einen Fehler gefunden, ihn behoben und es erneut versucht. Laut Anthropic förderte diese Arbeit Hunderte von Fehlern zutage, darunter einen Speicherzugriffsfehler in einem Dekompressor, der nur bei Eingaben von etwa 20 MB mit einem seltenen Layout auftrat, sowie die Wiederentdeckung eines bekannten Fehlers im libexpat-XML-Parser.
In separaten Tests bewies Claude, dass der zlib-Code des Linux-Kernels der Formatspezifikation entspricht. Bei der Überprüfung eines weit verbreiteten PDF-Readers fand er innerhalb einer Woche so viele Sicherheitslücken, wie üblicherweise in einem Jahr gemeldet werden. Details finden Sie in der [Referenz einfügen]. Technischer Anhang.
Was es nicht beweist
Anthropic stellt ausdrücklich klar, dass “formal verifiziert” nicht fehlerfrei bedeutet. Die Beweise basieren auf der Annahme von statisch gelinkten, einsträngigen RISC-V-Binärdateien unter Linux, während die meisten realen Anwendungen auf x86 oder ARM laufen. Die verwendeten Speicherprüfungen decken nicht alle Speichersicherheitslücken auf, und nicht jeder Einstiegspunkt in jeder Bibliothek wurde abgedeckt.
Die Kosten sind der zweite Haken: Beweise können Hunderte Millionen Tokens benötigen. Laut Anthropic löste Claude Opus 5.5 die Hälfte eines Benchmarks mit 36 Aufgaben mit etwa 40% weniger Tokens als Opus 5, und Agenten, die Beweise teilten, verbrauchten 17% weniger Tokens.
Warum es wichtig ist
KI wird immer besser darin, Fehler zu finden, wie die PHP2Shell-Schwachstellen Diese Woche wurde gezeigt, dass Beweise dazu dienen, zu zeigen, dass ganze Klassen von Fehlern schlichtweg nicht existieren. Theorem hat eine veröffentlicht. Claude Fähigkeit für Open-Source-Entwickler, die ihre Projekte anmelden möchten, und es Schätzungen dass 95% des Maschinencodes im Nix-Software-Ökosystem bis Ende 2027 für etwa $134 Millionen verifiziert werden könnten.
