Anthropic: Claude beweist Absturzfreiheit in 123 Open-Source-Bibliotheken

Vom Fuzz-Test zum Beweis

Formale Verifikation galt bisher als Luxus für Avionik und Kernel-Forschung: Beim seL4-Kernel kostete der Beweis rund zwanzig Personenjahre, die Implementierung nur zwei. Anthropics Frontier Red Team zeigt nun zusammen mit Theorem, dass LLMs diese Hürde drastisch senken.

Der Trick: Vorhandene Fuzz-Tests aus Googles OSS-Fuzz werden automatisch in eine Spezifikation übersetzt – „dieser Test stürzt für keine Eingabe unter 64 MB ab“. Claude beweist diese Aussage dann über den kompilierten RISC-V-Binärcode, nicht über den Quelltext.

Die Zahlen

• 239 Entry Points in 123 Bibliotheken bewiesen, innerhalb weniger Wochen
• rund 180 Millionen Zeilen Rocq-Beweiscode, typischer Beweis ca. 600.000 Zeilen
• Annahmen: single-threaded, statisches Binary, festes Speicherbudget, Linux auf RISC-V

Prüfen muss man den Beweis nicht von Hand: Vertrauen muss man nur den Modellen von RISC-V und Linux-Prozessen, den Theorem-Aussagen und dem Rocq-Checker.

Bugs, die kein Fuzzer findet

Beim Beweisversuch fand Claude Fehler und patchte sie selbst, bevor der Beweis gelang: einen Zähler-Underflow in einem Dekompressor mit Out-of-Bounds-Write (nur bei ca. 20-MB-Eingaben mit seltenem Layout), einen Out-of-Bounds-Read in einem Bilddecoder (64 MB Eingabe, über 2 GB RAM), eine Wiederentdeckung von CVE-2026-56132 in libexpat und einen Logikfehler, bei dem eine Dateizugriffs-Beschränkung nicht immer durchgesetzt wurde.

Anthropic veröffentlicht einen Teil der Beweise samt Semantik; Theorem bietet die Pipeline für andere Open-Source-Projekte an und stellt einen Claude-Skill bereit. Die Grenzen sind klar benannt: Das ist kein Beweis für Bugfreiheit schlechthin, sondern für eine definierte Eigenschaftsklasse unter klaren Annahmen.

Quelle: Anthropic Research