Anthropic weist formale Beweise in 123 Open-Source-Bibliotheken nach: 239 Einstiegspunkte ohne Crash bei Inputs bis 64 MB — 180 Millionen Zeilen Rocq und Bugfunde, die Trillionen Fuzzing-Läufen entgangen waren

Anthropic weist formale Beweise in 123 Open-Source-Bibliotheken nach: 239 Einstiegspunkte ohne Crash bei Inputs bis 64 MB — 180 Millionen Zeilen Rocq und Bugfunde, die Trillionen Fuzzing-Läufen entgangen waren — Am 22. Oktober veröffentlichte Anthropic mit dem Verifikationslabor Theorem den ersten großflächigen Einsatz formaler Verifikation auf Produktsoftware: bestehende OSS-Fuzz-Tests werden zu Spezifikationen umgebaut (kein Absturz, egal welcher Input bis 64 MB, bei jedem modellierten Linux-Antwortverhalten und jeder Speicherbelegung), Claude schreibt die Beweise gegen Theorems RISC-V- und Linux-Prozess-Semantik, der Rocq-Kernel prüft maschinell. Ergebnis: 239 Einstiegspunkte über 123 Bibliotheken abgesichert, die kompilierten Binaries halten median 18.000 RISC-V-Instruktionen, ein typischer Beweis umfasst rund 600.000 Zeilen, zusammen etwa 180 Millionen; Annahmen bleiben single-threaded statische Binaries mit fixem Speicherbudget (musl) auf RISC-V. Entdeckt wurden dabei hunderte Fehler, die Trillionen Fuzzing-Läufen entgangen waren: ein Counter-Underflow in einem Dekompressor erst bei rund 20 MB mit seltenem Layout, ein Out-of-Bounds-Read in einem Bild-Decoder erst bei 64-MB-Eingang und mehr als 2 GB Speicher, in libexpat die Wiederentdeckung von CVE-2026-56132; ein verbreiteter PDF-Leser lieferte in einer Woche so viele Sicherheitsbugs wie sonst in einem Jahr. Proof-Subset und Semantiken liegen auf GitHub, Theorem bietet die Pipeline für weitere Projekte und eine Claude-Skill. Randresultate: ein in Rust geschriebener Python-Interpreter, per Verus geprüft, traf CPython bei 1,7 Millionen Zufallsprogrammen zu 99,95 Prozent. Anthropic Research · LAVX · 🗃 Wayback Machine (Archiv)