Anthropic berichtet über formale Beweise für 239 Einstiegspunkte in 123 Bibliotheken

Der Claude-Anbieter Anthropic hat am 22. Oktober 2026 mit dem Partner Theorem einen Forschungsbericht zu formalen Software-Beweisen veröffentlicht. Laut Anthropic bewies Claude, dass 239 Einstiegspunkte in 123 OSS-Fuzz-Bibliotheken bei keiner Eingabe unter 64 MB abstürzen, nachdem es zuvor gefundene Fehler gepatcht hatte.

Die Beweise beziehen sich auf die kompilierten RISC-V-Instruktionen, also auf ausführbare Binaries. Anthropic nennt dafür feste Annahmen: ein einzelthreadiges statisches Programm mit festem Speicherbudget auf einer RISC-V-CPU unter Linux.

Laut Anthropic umfassen die Beweise rund 180 Millionen Zeilen Rocq. Ein typischer Beweis kommt auf etwa 600.000 Zeilen, die abgesicherten Binaries sind im Median 18.000 RISC-V-Instruktionen lang.

Die Zahlen sind groß. Ihre Aussagekraft hängt an der Spezifikation.

Vom Fuzz-Test zur Spezifikation

Anthropic beschreibt das Verfahren so: Entwickler übersetzen ihren Code in ein mathematisches Modell und versuchen zu beweisen, dass er stets einem festgelegten Satz von Sicherheitsregeln folgt.

Ausgangspunkt waren Fuzz-Tests. Ein Einstiegspunkt ist dabei eine Eingangstür in den Code, die die Autoren zum Testen bereitstellen. Der Fuzzer erzeugt dort enorme Mengen halbzufälliger und mutierter Eingaben, um einen Fehler zu finden. Eine Garantie, jeden möglichen Codepfad zu durchlaufen, gibt es dabei nicht, egal wie viele Eingaben er probiert.

Anthropic hat deshalb den Fuzz-Test in eine Spezifikation über die kompilierten RISC-V-Instruktionen umgewandelt. Sie besagt: kein Absturz bei Eingaben unter 64 MB. Damit Speicherfehler überhaupt als Absturz sichtbar werden, instrumentiert OSS-Fuzz C- und C++-Programme automatisch mit AddressSanitizer (ASan).

Absturzfreiheit bedeutet hier also immer: absturzfrei gegenüber genau dieser Spezifikation.

Fehlerfunde, Reward Hacking und Tokenkosten

Schon der Beweisversuch lieferte laut Anthropic Hunderte Fehler. Ein Beispiel ist ein Zähler-Unterlauf in einem Dekompressor, der zu einem Schreibzugriff außerhalb der Speichergrenzen führte. Er trat nur bei Eingaben von etwa 20 MB mit einem seltenen, spezifischen Aufbau auf. Fuzzer mutieren dagegen typischerweise kleine Eingaben bis 1 MB.

Weil Claude Code patchen durfte, benennt Anthropic selbst die Gefahr von Reward Hacking. Claude hätte jedes Theorem beweisbar machen können, indem es das Programm in eines umschreibt, das trivial nie abstürzt. Dagegen wurden Patches bestraft, protokolliert und auf solche Fehlermuster geprüft.

Billig ist das nicht. Die Beweise können laut Anthropic Hunderte Millionen Tokens kosten, der Bericht zählt das zu den zentralen Grenzen. Teilen hilft. In einem Experiment des Berichts durften Agenten Beweise aus einem gemeinsamen Arbeitsbereich voneinander kopieren; ihr Tokenbedarf sank dabei um 17 Prozent gegenüber Agenten, die allein arbeiteten.

Die Rolle des Rocq-Prüfers

Die Arbeitsteilung ist klar: Claude schreibt den Beweis, der Rocq-Kernel prüft ihn gegen die Spezifikation. Deshalb muss laut Anthropic praktisch nichts von dem umfangreichen Beweiscode von Hand gesichtet werden.

Vertrauen musst du danach den formalen Modellen von RISC-V und Linux-Prozessen, den exakt bewiesenen Theoremaussagen und dem Rocq-Prüfer selbst. Eine Fußnote ergänzt, dass technisch auch Hardware, Betriebssystem und OCaml-Compiler vertraut werden muss, auf denen der Prüfer aufsetzt.

Wenn Anthropic von einem externen Proof-Checker spricht, ist separate Prüfsoftware gemeint, keine unabhängige Studie. Eine unabhängige Prüfung der Beweise begrüßt Anthropic ausdrücklich.

Der Prüfer beantwortet eine präzise Frage: Erfüllt der Beweis die Spezifikation? Ob die Spezifikation die reale Maschine korrekt beschreibt, prüft er nicht.

Absturzfrei heißt nicht fehlerfrei

Anthropic formuliert es selbst: „Formally verified“ bedeutet nicht „bug-free“.

Hier wird die Modellannahme konkret. Die Beweise gelten für statische RISC-V-Binaries mit musl libc. Die meisten Nutzer betreiben diese Bibliotheken laut Bericht dagegen auf x86 oder ARM und linken sie dynamisch gegen glibc.

Hinzu kommt: ASan erkennt nicht alle Speichersicherheitsfehler, und nicht alle Einstiegspunkte jeder Bibliothek wurden verifiziert. Programme, die eine Bibliothek falsch verwenden, können außerdem Speicherbeschädigungen beim Aufrufer verursachen. Verbleibende Fehler liegen nach Anthropics Darstellung entweder in den vertrauten Komponenten oder außerhalb des Beweisumfangs.

Ein hypothetisches Beispiel: Ein Agent soll entscheiden, ob er eine der verifizierten Bibliotheken in einem x86-Dienst mit glibc ungeprüft übernehmen darf. Eine Garantie für diesen Build gibt der Bericht nicht her.

Was öffentlich prüfbar ist

Anthropic veröffentlicht laut Bericht eine Teilmenge der Beweise, damit andere sie prüfen und wiederverwenden können. Beweise, die einen ungepatchten Fehler in der Open-Source-Software offenlegen könnten, gibt Anthropic nicht frei.

Der öffentliche Teil ist überschaubar. Im Repository theorem-labs/oss-verify-proofs stellt Theorem Beweise für 60 Einstiegspunkte in 25 Bibliotheken bereit. Anthropics Gesamtversuch umfasste 239 Einstiegspunkte.

Auch für diesen Ausschnitt zieht Theorem die Grenzen eng. Ein Beweis besagt dort nicht, dass die Bibliothek korrekt ist; Fehler, die Sanitizer nicht erkennen, etwa falsche Ergebnisse oder Speicherlecks, sind nicht ausgeschlossen.

Offen bleibt auch das Programmende. Keiner der veröffentlichten Beweise schließt einen Lauf aus, der nie endet. Ein absturzfreies Binary kann also trotzdem endlos weiterlaufen.

Die veröffentlichten Beweise lassen sich nachrechnen. Theorems Prüflauf gleicht jedes Binary mit seinem SHA-256-Wert ab und kompiliert jeden Beweis. Annahmen außerhalb der Liste erlaubter Axiome weist er zurück. Öffentlich prüfbar heißt aber noch nicht unabhängig bestätigt.

Zum Weiterlesen: Claude formalisiert Fermats letzten Satz in elf Tagen sowie AWS-Benchmark: Frontier-Modelle verfehlen das Doppelziel der Schwachstellensuche.

Absturzfreiheit gilt nur für die bewiesenen Binaries

• Die Beweise gelten für die bewiesenen Einstiegspunkte, Eingaben unter 64 MB und das RISC-V-Linux-Modell.
• Absturzfreiheit lässt sich nicht auf x86-, ARM- oder glibc-Builds übertragen, solange für genau diese Binaries ein eigener Beweis fehlt.