Formale Verifikation mit Claude: Beweise für 123 Open-Source-Bibliotheken

Am 22. Oktober hat das Frontier Red Team von Anthropic zusammen mit der Firma Theorem eine Studie veröffentlicht, in der Claude formale Sicherheitsbeweise für 123 Open-Source-Bibliotheken aus dem Projekt OSS-Fuzz geschrieben hat. Die Beweise beziehen sich auf kompilierten RISC-V-Code, nicht auf den Quellcode. Laut den Autoren ist es die erste formale Verifikation von Produktionssoftware auf Assembler-Ebene mit Hilfe von KI in dieser Größenordnung.

Wie funktioniert formale Verifikation mit Claude?

Formale Verifikation ist ein mathematischer Beweis, dass ein Programm eine bestimmte Eigenschaft für jede mögliche Eingabe hat, nicht nur für die getesteten. Das Problem: Bisher brauchte sie jahrelange Arbeit von Experten. Ein Vergleich aus der Studie: Die Verifikation des seL4-Kernels dauerte etwa 20 Personenjahre, das Schreiben des Kernels zwei.

Die Pipeline aus der Studie sieht so aus:

1. Ausgangspunkt sind bestehende Fuzz-Tests aus OSS-Fuzz (einem Google-Projekt, das Bibliotheken ununterbrochen mit Zufallsdaten bombardiert).
2. Die Bibliothek wird zusammen mit dem Test zu einer RISC-V-Programmdatei kompiliert.
3. Aus Theorems Semantik des RISC-V-Prozessors und eines Linux-Prozesses entsteht automatisch eine Spezifikation: Das Programm muss immer normal beendet werden, ohne Speicherfehler und ohne fehlgeschlagene Assertions.
4. Claude schreibt den Beweis, und der Rocq-Beweisprüfer bestätigt, dass der Beweis die Spezifikation erfüllt.
5. Stößt Claude auf einen Fehler, patcht es den Code, die Spezifikation wird neu erzeugt und der Beweis entsteht von vorn.

Die Garantie gilt für jede Eingabe unter 64 MB und jede modellierte Systemantwort und Speicheranordnung (unter der Annahme eines statischen, single-threaded Programms auf RISC-V und Linux).

Welche Zahlen hat Anthropic genannt?

1. 239 Einstiegspunkte in 123 Bibliotheken.
2. Insgesamt rund 180 Mio. Zeilen Beweise in Rocq; ein typischer Beweis hat etwa 600.000 Zeilen und betrifft ein Programm mit im Median 18.000 RISC-V-Instruktionen.
3. Das Ganze dauerte einige Wochen.
4. Bei 36 kleinen Aufgaben bewies Opus 5.5 die Hälfte und verbrauchte dabei rund 40 % weniger Tokens als Opus 5; Agenten in einem gemeinsamen Arbeitsbereich verbrauchten 17 % weniger als allein.

Interessant: Der Beweis für cpp-httplib erforderte den Nachweis, dass der Rot-Schwarz-Baum in libc++ eine logarithmisch beschränkte Tiefe hat, denn nur so ließ sich ein Stack Overflow im Destruktor von std::set ausschließen.

Welche Fehler hat Claude gefunden?

Laut den Autoren hat der Prozess Hunderte Fehler aufgedeckt, die jahrelanges Fuzzing überstanden hatten. Beispiele aus dem Beitrag:

1. Ein Zähler-Underflow in einem Dekompressor, der zu einem Schreibzugriff außerhalb des Puffers führte, aber nur bei einer etwa 20 MB großen Eingabe mit seltenem Aufbau.
2. Ein Lesezugriff außerhalb des Puffers in einem Bilddecoder, der eine 64-MB-Eingabe und über 2 GB Speicher erforderte.
3. Ein Lesezugriff außerhalb des Puffers, der nur bei einer bestimmten Aufruffolge auf zwei Handles derselben Datei auftrat.
4. Die Wiederentdeckung von CVE-2026-56132 in libexpat (sie erforderte tief verschachtelte Eingaben).
5. Ein Logikfehler: Eine Funktion, die den Dateizugriff einschränkt, funktionierte nicht immer, obwohl nichts abstürzte.

Dazu kommen drei zusätzliche Experimente. Claude schrieb eine formale Spezifikation von RFC 1950 und bewies auf x86-Binärdateien, dass zlib aus dem Linux-Kernel sie korrekt implementiert. Außerdem baute es in Rust einen Interpreter für eine Teilmenge von Python, der sich bei 1,7 Mio. Zufallsprogrammen in 99,95 % der Fälle wie CPython verhielt. Und der Versuch, einen populären PDF-Reader zu verifizieren, fand in einer Woche so viele Sicherheitslücken, wie sonst in einem Jahr gemeldet werden.

Es ist dieselbe Richtung wie bei PHP2Shell und Claude Mythos bei der Bank of America: KI-Modelle finden Fehler, die Menschen und klassische Werkzeuge jahrelang übersehen haben. Nur endet es diesmal nicht bloß mit einem Patch, sondern mit einem Beweis.

Worauf sollten wir achten?

Erstens darauf, was „verifiziert“ bedeutet. Die Autoren schreiben klar, dass formale Verifikation keinen fehlerfreien Code bedeutet (im Original „»Formally verified« does not mean »bug-free.«“). Ein Beweis ist nur so gut wie die Spezifikation, die Modelle von RISC-V und Linux und der Rocq-Prüfer selbst.

Zweitens auf den Umfang. Die Beweise betreffen statische, single-threaded RISC-V-Binärdateien mit musl, während die meisten von uns Code auf x86 oder ARM mit glibc ausführen. Sie decken auch keinen toten Code ab und keine Fälle, in denen das aufrufende Programm den Speicher beschädigt.

Drittens auf die Kosten. Einzelne Beweise können Hunderte Millionen Tokens verschlingen, was die Autoren selbst als Haupteinschränkung bezeichnen.

Ein Teil der Beweise liegt bereits auf GitHub (oss-verify-proofs), zusammen mit der Semantik von RISC-V und Linux. Der Rest wartet noch, weil er ungepatchte Fehler offenlegen könnte.

FAQ

Was ist formale Verifikation?

Ein mathematischer, von einem Programm geprüfter Beweis, dass Code eine bestimmte Eigenschaft für alle Eingaben hat, z. B. dass er nie außerhalb eines Puffers schreibt. Tests und Fuzzing prüfen nur ausgewählte Fälle.

Sind die verifizierten Bibliotheken fehlerfrei?

Nein. Der Beweis garantiert die Abwesenheit von Abstürzen nur im beschriebenen Modell (RISC-V, Linux, Eingabe unter 64 MB, ein Thread). Fehler können in der Spezifikation, im Maschinenmodell oder außerhalb dieses Rahmens stecken.

Kann ich mein eigenes Projekt verifizieren lassen?

Theorem betreibt OSS Verify, ein kostenloses Programm für ausgewählte Open-Source-Projekte. Die Bewerbung reicht der Maintainer per Pull Request mit den Dateien project.yaml, Dockerfile und build.sh ein, ähnlich wie bei OSS-Fuzz. Man muss damit rechnen, den Build auf statische riscv64-Binärdateien umzustellen.