Formale Verifikation, also der mathematische Beweis, dass Code sich wie spezifiziert verhält, gilt seit Langem als Goldstandard der Sicherheit und als zu teuer für fast alle. Anthropic nennt ein anschauliches Beispiel: Der Kernel seL4 kostete zwei Personenjahre zum Schreiben und 20 zum Verifizieren. In Zusammenarbeit mit der Verifikationsfirma Theorem berichtet Anthropic nun, dass Claude solche Beweise in einem Umfang erstellt hat, der vor wenigen Jahren undenkbar gewesen wäre.
Der Kniff bestand darin, Spezifikationen nicht von Hand zu schreiben. Das Team nahm Fuzz-Tests aus Googles Programm OSS-Fuzz, kleine Einstiegspunkte, bei denen jeder Absturz als Fehler gilt, und machte aus jedem eine formale Aussage: Das kompilierte RISC-V-Binary stürzt bei keiner Eingabe unter 64 MB ab, auch nicht durch Speicherfehler, die AddressSanitizer erkennt. Binnen weniger Wochen bewies Claude dies für 239 Einstiegspunkte in 123 Bibliotheken und behob unterwegs die gefundenen Fehler. Die Beweise, überwiegend im Beweisassistenten Rocq, umfassen rund 180 Millionen Zeilen; ein typischer Beweis hat etwa 600.000 Zeilen für ein Binary mit im Median 18.000 Instruktionen. Lesen muss sie niemand; der Rocq-Prüfer bestätigt sie.
Die Fehler sind der unmittelbare Gewinn. Einige hätte ein Fuzzer kaum gefunden, etwa einen Schreibzugriff außerhalb der Grenzen in einem Dekompressor, der nur bei Eingaben von etwa 20 MB mit einem bestimmten Aufbau auftrat. Weitere Experimente bewiesen das zlib des Linux-Kernels gegen eine formale Fassung von RFC 1950 und prüften einen Rust-Interpreter für einen Teil von Python, der bei 99,95% von 1,7 Millionen Zufallsprogrammen mit CPython übereinstimmte. Auch die Kosten sinken: Bei 36 kleinen Aufgaben bewies Claude Opus 5.5 die Hälfte mit etwa 40% weniger Token als Opus 5, und geteilte Beweise zwischen Agenten sparten 17%.
Für Maintainer ist das der bisher stärkste Beleg, dass maschinell geprüfte Garantien für gängige Bibliotheken Routine werden könnten, so wie Fuzzing. Theorem bietet an, die Pipeline für weitere Open-Source-Projekte laufen zu lassen, und hat einen Claude-Skill veröffentlicht.
Die Autoren gehen mit den Grenzen sorgfältig um, und Leser sollten das auch. Verifiziert heißt nicht fehlerfrei. Die Beweise gelten für einfädige, statisch gegen musl gelinkte RISC-V-Builds, während die meisten Nutzer diese Bibliotheken auf x86 oder ARM mit glibc betreiben. AddressSanitizer übersieht manche Speicherfehler, nicht jeder Einstiegspunkt wurde abgedeckt, und Aufrufer können eine Bibliothek weiterhin falsch nutzen. Zudem können Beweise Hunderte Millionen Token kosten, und das ist die eigentliche Hürde für das gesamte Ökosystem.