LLMs und formale Verifikation: was „bewiesen“ bei 123 Bibliotheken heißt

Am 22. Oktober 2026 hat das Frontier Red Team von Anthropic zusammen mit einer Firma namens Theorem ein Ergebnis veröffentlicht, das du in Ruhe lesen solltest. Das Team hat Claude formale Beweise für echten Open-Source-Code auf Assembler-Ebene schreiben lassen, in 123 Bibliotheken, und dabei Bugs gefunden, die jahrelanges Testen überlebt hatten. Hier steht, was das einfach gesagt bedeutet, wo das Wort „bewiesen“ aufhört und was ein normales Team heute daraus mitnehmen kann.

Formale Verifikation ohne Fachjargon

Ein Test prüft die Eingaben, an die du gedacht hast. Ein Beweis deckt jede Eingabe ab. Bei formaler Verifikation übersetzt du Code in ein mathematisches Modell, schreibst Regeln auf, die er immer einhalten muss, und versuchst zu beweisen, dass das Modell sie einhält. Scheitert der Beweis, zeigt die Art des Scheiterns auf einen möglichen Bug. Du behebst ihn, versuchst es erneut und hast am Ende einen Beweis, dass kein Bug mehr übrig ist, der diese Regeln verletzt.

Der Haken war immer der Aufwand. Der Beitrag nennt das bekannte Beispiel: Der seL4-Kernel brauchte zwei Personenjahre für den Bau und 20 Personenjahre für die Verifikation. Deshalb blieb Verifikation in Bereichen wie Avionik-Code.

Was sie tatsächlich gemacht haben

Die Spezifikation zu schreiben ist meist das Schwerste, also haben sie eine verwendet, die es schon gab: die Fuzz-Tests aus Googles OSS-Fuzz. Ein Fuzz-Test ist ein Einstiegspunkt, der abstürzt, wenn etwas falsch ist, und ein Fuzzer bombardiert ihn mit riesigen Mengen generierter Eingaben. Er kann jahrelang laufen und ist trotzdem nie vollständig. Das Team hat jeden Fuzz-Test in eine Aussage verwandelt: Dieser Einstiegspunkt stürzt nie ab, für keine Eingabe unter 64 MB, auf dem kompilierten RISC-V-Binary.

Innerhalb weniger Wochen hat Claude die gefundenen Bugs gepatcht und diese Aussage für 239 Einstiegspunkte in 123 Bibliotheken bewiesen. Die Beweise umfassen zusammen etwa 180 Millionen Zeilen Rocq; ein typischer Beweis hat etwa 600.000 Zeilen, für Binaries mit im Median 18.000 RISC-V-Instruktionen. Das liest niemand von Hand. Das erledigt der Rocq-Beweisprüfer, und der Beitrag nennt, was du weiterhin glauben musst: die formalen Modelle von RISC-V und Linux-Prozessen, die genauen Theorem-Aussagen und den Prüfer selbst.

Auf die Bugs kommt es an

Fuzzer verändern kleine Eingaben, meist auf 1 MB begrenzt. Manches, was die Beweise zutage gefördert haben, liegt weit darüber: ein Zähler-Unterlauf in einem Dekompressor, der zu einem Schreibzugriff außerhalb der Grenzen führte, aber nur bei Eingaben um 20 MB mit einem seltenen Aufbau; ein Lesezugriff außerhalb der Grenzen in einem Bilddecoder, der eine 64-MB-Eingabe und über 2 GB Speicher brauchte; und die Wiederentdeckung von CVE-2026-56132 in libexpat. Ein Beweis hat außerdem einen Logikfehler aufgedeckt, der nie abstürzt: Eine Funktion, die einschränken soll, welche Dateien eine Anwendung laden darf, griff nicht immer. Der Punkt der Autoren: Schon der Versuch eines Beweises findet echte Bugs, ob er gelingt oder nicht.

Wo „bewiesen“ aufhört

Der Beitrag ist hier sehr direkt, und ich halte diesen Teil für den nützlichsten. „Formal verifiziert“ heißt nicht „fehlerfrei“. Es heißt, dass der Code die aufgeschriebenen Regeln einhält, auf der Maschine, die modelliert wurde. Zwei Lücken werden genannt:

• Die Maschine. Die Beweise gelten für statische, single-threaded RISC-V-Binaries, gelinkt gegen musl. Die meisten betreiben diese Bibliotheken auf x86 oder ARM, dynamisch gelinkt gegen glibc.
• Die Aussage. AddressSanitizer erkennt nicht jeden Speicherfehler, nicht jeder Einstiegspunkt wurde verifiziert, und ein Aufrufer kann die Bibliothek immer noch falsch benutzen.

Was das für ein normales Team bedeutet

Wahrscheinlich schreibst du demnächst kein Rocq. Aber die Methode beginnt bei etwas, das viele Teams schon haben: einem Test, der eine Eigenschaft ausdrückt. Ein Fuzz-Harness, das abstürzt, wenn ein Hin-und-zurück fehlschlägt, ist eine verkleidete Spezifikation, und der Beitrag merkt an, dass der Beweis, dass so ein Test nie abstürzt, dem Beweis der Eigenschaft selbst entspricht. Ein kleines Beispiel für die Form, zur Veranschaulichung und mit Platzhalter-Funktionsnamen:

#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/* your library's own functions; the names are placeholders */
size_t encode(const uint8_t *in, size_t n, uint8_t **out);
size_t decode(const uint8_t *in, size_t n, uint8_t **out);

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  uint8_t *packed = NULL, *back = NULL;
  size_t packed_n = encode(data, size, &packed);
  size_t back_n = decode(packed, packed_n, &back);
  assert(back_n == size && (size == 0 || memcmp(back, data, size) == 0));
  free(packed);
  free(back);
  return 0;
}

Tests dieser Art, bei denen ein Fehlschlag bedeutet, dass eine ausgesprochene Regel verletzt wurde, helfen dir heute schon mit einem gewöhnlichen Fuzzer, und genau so etwas kann diese Art von Werkzeug später in einen Beweis verwandeln. Theorem bietet nach eigener Aussage an, dieselbe Pipeline für andere Open-Source-Projekte laufen zu lassen, und veröffentlicht einen Claude-Skill, der Entwicklern den Einstieg in die Verifikation ihres eigenen Codes erleichtern soll.

Nächster Schritt: Nimm einen Parser oder Encoder aus deinem Code und schreib die Eigenschaft, die er immer einhalten muss, als Test, der laut fehlschlägt. Lies dann den Abschnitt über die Grenzen im Originalbeitrag, bevor du einem Etikett „formal verifiziert“ vertraust. Quelle: Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale.