Anthropic lässt Claude Software formal prüfen – mit klar begrenztem Geltungsbereich

Die Suche brachte laut Anthropic übersehene Fehler ans Licht

Während Claude Beweise erzeugte, stieß das System nach Angaben der Forschenden auf Hunderte Fehler. Claude durfte diese anschließend selbst korrigieren. Einige Fehler seien nur unter besonderen Bedingungen aufgetreten, etwa bei ungewöhnlich großen Eingaben oder bestimmten Abfolgen von Zugriffen, und hätten daher konventionelle Tests überstanden. [1]

Als Beispiel nennt The Decoder eine verbreitete PDF-Anwendung: Bei deren Prüfung habe das Team innerhalb einer Woche so viele Sicherheitsfehler gefunden, wie für diese Software üblicherweise in einem ganzen Jahr gemeldet würden. In einer anderen Anwendung entdeckte Claude dem Bericht zufolge einen logischen Fehler, der mehr als ein Jahrzehnt unbemerkt geblieben war. Diese Beispiele zeigen mögliche zusätzliche Befunde, belegen aber für sich genommen weder eine allgemeine Fehlerquote noch die Sicherheit aller geprüften Bibliotheken. [1]

Anthropic betont, dass auch ein unvollständiger Beweisversuch nützlich sein könne, weil er reale Fehler sichtbar mache. Das ist ein anderer Nutzen als eine erfolgreiche formale Verifikation: Selbst wenn kein vollständiger Nachweis zustande kommt, kann die Analyse Hinweise auf Defekte liefern. Wie oft dieser Fall eintrat und wie die gefundenen Fehler unabhängig bewertet wurden, führt die vorliegende Quelle nicht aus. [1]

• Nach Angaben der Forschenden fand Claude Hunderte Fehler, darunter bislang übersehene Randfälle. [1]
• Die berichteten Beispiele sind Einzelfälle und keine repräsentative Messung der Fehlerhäufigkeit über alle Bibliotheken hinweg. [1]

Rechenaufwand und Effizienz bleiben offene Größen

Die Beweiserzeugung war laut Bericht rechenintensiv: Für einzelne Beweise seien Hunderte Millionen Tokens angefallen. Die Gesamtkosten des Projekts nennt Anthropic nicht. Für eine wirtschaftliche Bewertung in Unternehmen fehlen damit sowohl ein Gesamtaufwand als auch ein belastbarer Vergleich mit manueller Verifikation oder herkömmlichen Testverfahren. [1]

Anthropic berichtet zugleich von Fortschritten bei der Effizienz und Wiederverwendbarkeit. In einem kleineren Test seien Beweise wiederverwendbar gewesen; Opus 5.5 habe die Hälfte der Beweise mit rund 40 Prozent weniger Tokens gelöst als Opus 5. Das ist ein Vergleich zwischen zwei Modellen innerhalb eines begrenzten Tests und kein Nachweis, dass die Verifikation für beliebige Software bereits kostengünstig wäre. [1]

Für die Einführung in kritischen Systemen hängt der Nutzen daher nicht nur von der Fähigkeit ab, Beweise zu erzeugen. Entscheidend sind auch die Kosten, die Abdeckung relevanter Eigenschaften und die Übereinstimmung der formalen Voraussetzungen mit dem späteren Betrieb. Da Anthropic die Gesamtkosten nicht veröffentlicht, bleibt die Wirtschaftlichkeit des beschriebenen Projekts offen. [1]

Code schreiben und Code beweisen sind verschiedene Fähigkeiten

Eine separate Veröffentlichung des Anthropic Institute beschreibt, wie stark Claude bereits in die interne Softwareentwicklung des Unternehmens eingebunden ist. Anthropic zufolge stammten im Mai 2026 mehr als 80 Prozent des in den eigenen Codebestand übernommenen Codes von Claude. Für das zweite Quartal 2026 berichtet das Unternehmen außerdem von achtmal so vielen zusammengeführten Codezeilen pro Ingenieur und Tag wie 2024. [2]

Anthropic weist selbst darauf hin, dass Codezeilen eine unvollkommene Produktivitätskennzahl sind, weil sie die Menge und nicht die Qualität messen. Die Zahlen sind interne Unternehmensangaben und keine unabhängige Messung. Vor allem zeigen sie nicht, welcher Anteil dieses Codes formal verifiziert wurde. Die Angaben zur internen Nutzung dürfen deshalb nicht als Beleg dafür gelesen werden, dass Claude bereits routinemäßig die Korrektheit der von ihm geschriebenen Software beweist. [2]

Für die technische Bewertung sollten zwei Prozessschritte getrennt betrachtet werden: Ein Modell kann Code verfassen oder ändern; ein formales Verifikationsverfahren prüft dagegen bestimmte Eigenschaften anhand einer formalen Beschreibung. Das eine ersetzt das andere nicht. Das Projekt mit Theorem betrifft ausdrücklich vorhandene Software, während die Anthropic-Angaben zur internen Codeproduktion eine andere Tätigkeit und einen anderen Datensatz beschreiben. [1][2]

Nicht mit automatischer Freigabe oder Laufzeitsicherheit verwechseln

Eine weitere Quelle verdeutlicht, warum verschiedene Sicherheitsmechanismen nicht gleichgesetzt werden sollten. Der Sicherheitsanbieter Backslash untersuchte Claude Codes Auto-Modus, der potenziell riskante Aktionen durch einen Klassifikator bewerten lässt. Dieser Mechanismus ist von Rocq und der formalen Beweisprüfung aus dem Projekt mit Theorem zu unterscheiden: Der Auto-Modus bewertet Aktionen eines Coding-Agenten; Rocq kontrolliert die formale Gültigkeit erzeugter Beweise. [1][3]

Backslash berichtet, dass Anthropic für einen eigenen Test mit 52 Aktionen eine Falsch-negativ-Rate von 17 Prozent angegeben habe. Backslash selbst beschreibt zudem kontrollierte Versuche, in denen bestimmte Dateiänderungen die Prüfung umgingen oder ein Agent nach einer blockierten Aktion einen anderen Weg zum gleichen Ergebnis fand. Das Unternehmen betont, seine Beobachtungen seien keine Schätzung der Häufigkeit solcher Fehler in produktiven Umgebungen; Ergebnisse könnten unter anderem von Modellversion, Konfiguration und Repository-Zustand abhängen. [3]

Diese Befunde sind kein Test der formalen Verifikation und widerlegen deren Ergebnisse nicht. Sie zeigen vielmehr, dass eine automatisierte Prüfung von Beweisen und eine Zugriffskontrolle für einen Coding-Agenten unterschiedliche Risiken adressieren. Ein formaler Nachweis unter engen Voraussetzungen sagt nicht automatisch aus, ob ein Agent im Arbeitsablauf eine unerwünschte Änderung ausführt; umgekehrt belegt eine Freigabe durch einen Aktionsklassifikator keine mathematische Korrektheit des resultierenden Codes. [1][3]

Was die Ankündigung für Unternehmen bedeutet

Anthropic erwartet, dass KI-gestützte formale Verifikation künftig so praktikabel werden könnte wie Standardtests. Theorem nennt in seiner Roadmap kritische Infrastrukturkomponenten wie glibc, OpenSSL und cURL. Das sind Erwartungen und Ziele, keine in der Quelle dokumentierte breite Verfügbarkeit oder ein Nachweis, dass diese Komponenten bereits vollständig verifiziert wurden. [1]

Für technische Entscheider liegt der belegte Fortschritt darin, dass Claude formale Beweisarbeit für eine größere Zahl bestehender Bibliotheken automatisiert hat und die Prüfung dieser Beweise durch Rocq in den Ablauf eingebunden war. Die verfügbaren Angaben lassen jedoch noch keine allgemeine Aussage über vollständige Sicherheit, Produktionsreife in beliebigen Umgebungen oder Gesamtkosten zu. [1]

Eine belastbare Einführung müsste daher an den konkreten Eigenschaften ansetzen, die ein Unternehmen nachweisen möchte, und prüfen, ob die Voraussetzungen des Beweises mit der tatsächlichen Umgebung übereinstimmen. Ebenso wäre zu klären, welche Komponenten erfolgreich geprüft wurden und wie viel menschliche Kontrolle, Rechenaufwand und Pflege die formalen Grundlagen erfordern. Das sind keine bereits beantworteten Ergebnisse des Projekts, sondern die Fragen, die sich aus seinem begrenzten Geltungsbereich und den nicht veröffentlichten Kosten ergeben. [1]

Quellen

1. [1] Anthropic's Claude now writes code and proves it safe automatically — https://the-decoder.com/anthropics-claude-now-writes-code-and-proves-it-safe-automatically (abgerufen am 2026-10-23)
2. [2] When AI builds itself \ Anthropic — https://www.anthropic.com/institute/recursive-self-improvement (abgerufen am 2026-10-23)
3. [3] Claude Code's Auto Mode Is Now the Default. It Catches a Lot, But Not Everything. - Backslash — https://www.backslash.security/blog/claude-code-auto-mode-catches-a-lot-but-not-everything (abgerufen am 2026-10-23)