Anthropics Frontier Red Team hat am 22. Oktober einen Bericht veröffentlicht, der formale Verifikation aus der Nische holt. Gemeinsam mit der Firma Theorem hat das Team Claude Sicherheitseigenschaften für 239 Einstiegspunkte in 123 Open-Source-Bibliotheken beweisen lassen – auf Ebene des übersetzten RISC-V-Maschinencodes.
Warum das bisher niemand gemacht hat
Formale Verifikation übersetzt Code in ein mathematisches Modell und beweist dann, dass er bestimmte Regeln nie verletzt. Das Verfahren ist alt und zuverlässig, aber teuer: Der Betriebssystemkern seL4 brauchte zwei Personenjahre für die Umsetzung und zwanzig für den Beweis. Entsprechend findet man es bei Airbus-Avionik und sonst fast nirgends.
Anthropics Ausgangspunkt ist ein anderes Problem. Modelle finden Fehler inzwischen schneller, als Tests sie abdecken: Im Linux-Kernel, einer der bestgetesteten Codebasen überhaupt, wurden kürzlich über 1.000 Schwachstellen offengelegt. Wer nicht hinterherlaufen will, braucht einen Beweis statt eines Testlaufs.
Fuzz-Tests als Spezifikation
Der Trick des Projekts besteht darin, keine Spezifikation zu schreiben. Statt zu definieren, was ein Programm tun soll, nimmt das Team vorhandene Fuzz-Tests aus Googles OSS-Fuzz und verwandelt die Regel „dieser Test stürzt nie ab“ in die Spezifikation. Gelingt der Beweis, ist das Fuzzing dieses Einstiegspunkts überflüssig: Es kann dort keinen Absturz mehr finden.
Bewiesen wurde konkret, dass die Programme bei jeder Eingabe unter 64 Megabyte normal beenden, ohne Speicherfehler und ohne verletzte Zusicherung, und das unter der Annahme eines einzelnen Threads, eines statischen Binaries mit festem Speicherbudget auf einer RISC-V-CPU unter Linux. Die Beweise umfassen rund 180 Millionen Zeilen Rocq, ein typischer Beweis etwa 600.000 Zeilen für ein Binary mit im Mittel 18.000 RISC-V-Instruktionen.
Prüfen muss das niemand von Hand. Der Rocq-Kern kontrolliert jeden Beweis gegen die Spezifikation. Vertrauen müssen Entwickler nur drei Dinge: die formalen Modelle von RISC-V und von Linux-Prozessen, die bewiesenen Theoremaussagen und den Rocq-Prüfer selbst.
Die Fehler, die kein Fuzzer findet
Unterwegs kamen Hunderte Bugs heraus, und einige davon sind der eigentliche Gewinn. Fuzzer mutieren kleine Eingaben, üblicherweise bis ein Megabyte. Claude fand in einer mitkopierten Dekompressor-Variante einen Zähler-Unterlauf, der zu einem Schreibzugriff außerhalb des Speichers führt – aber nur bei rund 20 Megabyte Eingabe mit einem seltenen Layout. Ein anderer Lesefehler brauchte 64 Megabyte Eingabe und über zwei Gigabyte Arbeitsspeicher. Dazu kam eine Wiederentdeckung von CVE-2026-56132 in libexpat und ein Logikfehler, der nie abstürzt: Eine Funktion, die begrenzen soll, welche Dateien eine Anwendung laden darf, griff nicht immer.
Der Engpass ist nicht mehr die Expertise
Anthropic veröffentlicht einen Teil der Beweise samt RISC-V- und Betriebssystem-Semantik, und Theorem bietet an, die Pipeline für andere Open-Source-Projekte laufen zu lassen, mitsamt einem Claude-Skill für den Einstieg.
Bemerkenswert ist der Satz am Ende des Berichts: Wer formale Verifikation mit schwächeren Modellen probiert hat und aufgegeben hat, soll es noch einmal versuchen. Dieselbe Richtung zeigen die 493 Funde der Attack Surface Reduction vom Vortag. Beweisen bleibt teuer, aber die Kosten liegen jetzt bei Rechenzeit statt bei Personenjahren, und Rechenzeit skaliert.