Anthropic zufolge hat Claude formale Beweise dafür erstellt, dass 123 Open-Source-Bibliotheken nicht abstürzen

In Zusammenarbeit mit Theorem gibt Anthropic an, Claude verwendet zu haben, um Sicherheitseigenschaften auf Assembly-Ebene (RISC-V) in über 100 Open-Source-Bibliotheken aus der Praxis zu beweisen. Das Unternehmen bezeichnet dies als den ersten groß angelegten Einsatz von KI zur formalen Verifikation von Produktivsoftware auf dieser Ebene.

Laut Anthropic:

• Was bewiesen wurde: Bei 239 Fuzz-Test-Einstiegspunkten in 123 OSS-Fuzz-Bibliotheken beenden die Programme ihre Ausführung für jede Eingabe unter 64 MB stets ordnungsgemäß – ohne Speicherfehler oder fehlgeschlagene Assertions. Dies gilt unter bestimmten Annahmen: eine statische Binärdatei mit einem Thread und festem Speicherbudget auf einer RISC-V-CPU mit Linux. Die Beweise umfassen insgesamt etwa 180 Millionen Zeilen Rocq, die vom Rocq-Proof-Checker überprüft wurden.
• Wie: Der bestehende Fuzz-Test jeder Bibliothek wurde in eine Spezifikation umgewandelt („dieser Test stürzt nie ab“), und Claude verfasste den Beweis und behob dabei gefundene Fehler. Anthropic zufolge wurden so Hunderte von Fehlern entdeckt, darunter solche, die ein Fuzzer wahrscheinlich nicht erreichen würde, etwa ein Schreibzugriff außerhalb des zulässigen Speicherbereichs, der eine seltene 20-MB-Eingabe erfordert, sowie eine erneute Entdeckung von CVE-2026-56132 in libexpat.
• Weitere Experimente: Claude bewies auf Binärcodebene für x86, dass die zlib-Implementierung des Linux-Kernels einer Spezifikation von RFC 1950 entspricht, und entwickelte einen Python-Interpreter in Rust, dessen Verhalten bei 99,95 % von 1,7 Millionen zufälligen Programmen mit CPython übereinstimmte. Anthropic zufolge ergaben formale Verifikationsversuche bei einem weit verbreiteten PDF-Reader außerdem innerhalb einer Woche ebenso viele Sicherheitsfehler wie üblicherweise innerhalb eines Jahres gemeldet werden.
• Kosten: Beweise können Hunderte Millionen Tokens erfordern. Bei 36 kleinen Verifikationsaufgaben beweist Opus 5.5 laut Anthropic die Hälfte davon mit etwa 40 % weniger Tokens als Opus 5; außerdem benötigten Agents, die Beweise miteinander teilten, 17 % weniger Tokens.

Anthropic veröffentlicht eine Auswahl der Beweise sowie die RISC-V- und Linux-Semantik. Theorem bietet an, dieselbe Pipeline für andere Open-Source-Projekte auszuführen, und veröffentlicht einen Claude-Skill zur Verifikation des eigenen Codes. Anthropic weist darauf hin, dass dies nicht belegt, dass die Bibliotheken fehlerfrei sind: Verbleibende Fehler lägen in den vertrauenswürdigen Komponenten oder außerhalb des Umfangs der Beweise.