Anthropic hat Claude mathematische Sicherheitsbeweise für Software schreiben lassen und dabei hunderte Fehler gefunden. Was belegt ist, wo Anthropic selbst Grenzen nennt und was du fragst, wenn dir jemand „bewiesen sicher“ verspricht.
Am 22. Oktober 2026 hat Anthropic beschrieben, wie Claude in einigen Wochen mathematische Sicherheitsbeweise für 123 Open-Source-Bibliotheken geschrieben hat. Wir haben den Beitrag gelesen und ordnen ein, was er belegt, wo Anthropic selbst Grenzen nennt und was das für Betriebe heißt, die Software und Dienstleister einkaufen.
Das Frontier Red Team von Anthropic hat gemeinsam mit der Firma Theorem Claude Sicherheitseigenschaften für 123 Open-Source-Bibliotheken beweisen lassen, gestützt auf 239 Einstiegspunkte aus Googles Fuzz-Testsammlung OSS-Fuzz. Bewiesen wurde, dass diese Programme bei Eingaben unter 64 Megabyte nicht abstürzen, also keine Speicherfehler und keine fehlgeschlagenen Prüfungen im Code auftreten. Die Beweise umfassen nach Anthropic rund 180 Millionen Zeilen in der Beweissprache Rocq, ein typischer Beweis etwa 600.000 Zeilen, und sie entstanden in einigen Wochen.
Formale Verifikation heißt: Man beschreibt in einer Spezifikation genau, was ein Programm tun oder nie tun darf, und beweist mathematisch, dass der Code das einhält. Bisher war das extrem aufwendig. Anthropic nennt als Beispiel den seL4-Kernel mit zwei Personenjahren für die Umsetzung und 20 Personenjahren für die Verifikation. Eingesetzt wurde es vor allem dort, wo Fehler sehr teuer sind, etwa in der Flugzeugelektronik. Neu ist laut Anthropic, dass ein KI-Modell solche Beweise in diesem Umfang schreibt, nach eigener Angabe die erste groß angelegte Anwendung dieser Art auf Binärcode-Ebene.
Beim Beweisen fand Claude hunderte Fehler und behob manche selbst. Genannt werden ein Zählerfehler in einem Dekomprimierer, der bei rund 20 Megabyte Eingabe außerhalb des Speicherbereichs schreibt, ein Lesefehler in einem Bilddecoder und die Wiederentdeckung der bekannten Lücke CVE-2026-56132 in der Bibliothek libexpat. Bei der Kompressionsbibliothek zlib wurde die Version aus dem Linux-Kernel gegen die Spezifikation RFC 1950 bewiesen, dort fanden sich nur kleine, nicht ausnutzbare Randfälle.
Das sind Herstellerangaben aus Anthropics eigenem Beitrag. Wir haben ihn gelesen, aber weder die Beweise noch die Bibliotheken geprüft. Nach dem Beitrag wurden die Beweise nicht extern begutachtet. Ein Teil davon soll zur Prüfung auf GitHub veröffentlicht werden, Beweise, die noch nicht behobene Fehler offenlegen würden, bleiben zurück.
Anthropic schreibt selbst, „formally verified“ bedeute nicht „bug-free“. Ein Beweisprüfer kann nur feststellen, ob der Code zur Spezifikation passt, nicht ob die Spezifikation zur Wirklichkeit passt. Die Beweise gelten außerdem nur für ein enges Setup: statische, nicht parallel laufende RISC-V-Programme mit der Bibliothek musl unter Linux, während reale Systeme oft x86 oder ARM mit glibc nutzen. Dazu kommt, dass ein Speicherprüfer nicht alle Fehler erkennt, nicht alle Einstiegspunkte geprüft wurden und falsche Nutzung durch aufrufende Programme nicht abgedeckt ist. Anthropic nennt auch das Risiko, dass Claude ein Programm so umschreibt, dass es trivial nie abstürzt, deshalb wurden solche Änderungen bestraft und protokolliert.
Für Betriebe heißt das: Wirbt ein Anbieter oder Dienstleister mit „geprüft“, „verifiziert“ oder „bewiesen sicher“, ist die Frage nicht ob, sondern was genau. Ein Beweis, dass eine Bibliothek nicht abstürzt, sagt zum Beispiel nichts darüber, ob jemand Schadcode in ein ausgeliefertes Paket einschleust, wie beim Angriff auf LiteLLM. Das ist unsere Einordnung und nicht Teil von Anthropics Beitrag.
Dass eine KI Beweise in diesem Umfang schreibt und dabei konkrete Fehler findet, ist mehr als ein Laborversuch. Anthropic erwartet, dass Verifikation bald so praktikabel wird wie heute das Fuzzing, das ist aber eine Prognose und keine Zusage, und Kosten in Euro oder Dollar nennt der Beitrag nicht. Für deinen Betrieb ändert sich heute nichts, aber die Frage nach dem Prüfumfang wird dir häufiger begegnen.
Zwei Minuten: Schreib auf, mit welchem Wort der Anbieter wirbt, etwa „geprüft“, „zertifiziert“ oder „bewiesen“. Drei Minuten: Frag per Mail, was genau geprüft wurde, nach welcher Vorgabe und für welche Version, und bitte um den Bericht. Drei Minuten: Prüfe, ob eine unabhängige Stelle beteiligt war und ob das Datum zu der Version passt, die du einsetzt. Zwei Minuten: Notiere, was ausdrücklich nicht geprüft wurde, und entscheide, ob dich das stört. Ohne Bericht hast du nicht mehr als ein Versprechen.
Anthropic zeigt, dass eine KI formale Beweise in großem Umfang schreiben kann und dabei echte Fehler findet. Zugleich schreibt Anthropic selbst, dass „bewiesen“ nicht „fehlerfrei“ heißt.
Für deinen Betrieb gilt: Verspricht dir jemand „bewiesen sicher“, frag nach Eigenschaft, Vorgabe, Version, unabhängiger Prüfung und Ausnahmen.
Quelle: Anthropic Frontier Red Team, „LLMs are making formal software verification feasible at a much larger scale“ (22. Oktober 2026), gelesen am 23. Oktober 2026 und sinngemäß aus dem Englischen wiedergegeben. Ein Teil der Beweise liegt laut Beitrag bei Theorem auf GitHub, wir haben ihn nicht geprüft. Alle Zahlen sind Herstellerangaben. Die Einordnung für Betriebe, die Fragen und der Prüfsatz sind unsere und nicht Teil des Beitrags.
Welches Modell für welche Aufgabe, welche Tools wirklich zählen und wie du richtig promptest — komplett lesbar, kein Download.
Jetzt gratis lesen →Wir gehen mit dir die Zusagen deiner Software-Anbieter und Dienstleister durch, trennen Werbeversprechen von Belegen und legen fest, welche Fragen du stellst.