Claude schreibt mathematische Beweise fuer die Korrektheit von Open-Source-Code
Anthropic hat Claude rund 180 Millionen Zeilen Beweiscode fuer 123 Open-Source-Bibliotheken erzeugen lassen. Dabei fand das Modell Fehler, die jahrelange Tests uebersehen hatten. Ziel ist, formale Verifikation mit AI zur Routine zu machen.
Anthropic hat mit Claude mathematisch bewiesen, dass bestehender Code korrekt ist. Der Ansatz greift ein Kernproblem KI-generierter Software auf, stoesst jedoch an strenge praktische Grenzen.
Den Nachweis zu fuehren, dass Software unter allen Umstaenden fehlerfrei laeuft, war bislang prohibitiv teuer. Ein Team von Spezialisten benoetigte rund 20 Personenjahre, um allein den kleinen Betriebssystemkern seL4 formal zu verifizieren, weshalb die Methode extremen Faellen wie der Avioniksoftware von Airbus vorbehalten blieb.
Anthropics Frontier Red Team liess gemeinsam mit dem Partner Theorem stattdessen Claude die Beweisarbeit uebernehmen. Das Modell erzeugte in nur wenigen Wochen rund 180 Millionen Zeilen mathematischen Beweiscodes und stuetzte sich dabei auf Testprogramme aus 123 Open-Source-Bibliotheken des Sicherheitsprojekts OSS-Fuzz von Google.
Statt neuen Code zu schreiben, verifizierte Claude bestehende Software, indem es Crashtests in mathematische Probleme uebersetzte, den kompilierten Maschinencode analysierte und umfangreiche Beweise erstellte. Ein unabhaengiges Verifikationsprogramm namens Rocq prueft diese Beweise automatisch, und laut Anthropic benoetigt der Prozess kaum menschliche Pruefer. Die Forscher bezeichnen das als vollautonomes, "fully autonomous", Beweismittel-Erzeugen, wobei die Werkzeuge und formalen Grundlagen allerdings von Menschen bei Theorem geschaffen wurden.
Waehrend der Beweisgenerierung stiess Claude auf hunderte Fehler und durfte diese selbst beheben. Viele waeren dem konventionellen Testen entgangen, weil sie sich nur unter sehr speziellen Bedingungen zeigen, etwa bei ungewoehnlich grossen Eingabedateien oder einer bestimmten Abfolge von Zugriffen, so die Forscher.
Bei dem Versuch, einen weit verbreiteten PDF-Reader zu verifizieren, fand das Team beispielsweise in einer Woche ebenso viele Sicherheitsluecken, wie fuer diese Software normalerweise in einem ganzen Jahr gemeldet werden. In einer anderen Anwendung entdeckte Claude einen logischen Fehler, der ueber ein Jahrzehnt lang unentdeckt geblieben war. Selbst wenn ein vollstaendiger Beweis am Ende scheitert, so Anthropic, bringe der Versuch dennoch echte Fehler ans Licht.
Anthropic raeumt ein, dass "formal verifiziert" nicht "fehlerfrei" bedeutet. Die Beweise gelten nur unter strengen Bedingungen: einer bestimmten Prozessorarchitektur, einsträngigen Programmen und Eingaben unter 64 MB. In der Praxis laufen diese Bibliotheken auf anderer Hardware und in anderen Konfigurationen.
Die Rechenkosten sind hoch, fuer einzelne Beweise werden hunderte Millionen Token verbraucht. Anthropics Gesamtprojektkosten nennt das Unternehmen nicht. Doch wenn KI ihren eigenen Code verifizieren kann, koennen Entwickler KI-generierter Software mehr vertrauen und weniger Zeit in deren Pruefung investieren. Das spart nicht nur bei der Verifikation Kosten, sondern im gesamten Programmierprozess. Ein kleinerer Testlauf zeigte zudem, dass Beweise wiederverwendbar sind, und neuere Modelle werden effizienter: Opus 5.5 loest die Haelfte der Beweise mit rund 40 Prozent weniger Token als Opus 5.
Das Projekt staerkt das Argument fuer die Automatisierung von Software. Wenn KI Code schreiben und dessen Korrektheit unter definierten Bedingungen garantieren kann, verschiebt sich die Frage von "Kann KI programmieren?" zu "Kann KI beweisen, dass der von ihr geschriebene Code sicher ist?" Faellt die Antwort ja aus, koennten die Konsequenzen weit ueber die heutigen Coding-Tools hinausgehen.
Ein Beleg dafuer: Anthropic erwartet, dass formale Verifikation mit KI bald so praktikabel wird wie Standardtests, und Theorems Roadmap zielt bereits auf kritische Infrastruktur wie glibc, OpenSSL und cURL ab.
Abonniere THE DECODER fuer werbefreies Lesen, einen woechentlichen KI-Newsletter, unseren exklusiven Frontier-Report "AI Radar" sechsmal im Jahr, vollen Archivzugang und Zugang zu unserem Kommentarbereich.
Automatisch übersetzt. Das Original auf Englisch ist unten aufklappbar.
Original (Englisch) anzeigen
Anthropic used Claude to mathematically prove that existing code is correct. The approach tackles a core problem with AI-generated software but comes with strict practical limits.
Proving that software runs error-free under all circumstances has always been prohibitively expensive. A team of specialists needed 20 person-years just to formally verify the small operating system kernel seL4, so the method was reserved for extreme cases like Airbus avionics software.
Anthropic's Frontier Red Team, working with partner Theorem, let Claude take over the proof work instead. The model produced roughly 180 million lines of mathematical proof code in just a few weeks, drawing on test programs from 123 open-source libraries in Google's OSS-Fuzz security project. Ad
Rather than writing new code, Claude verified existing software by translating crash tests into mathematical problems, analyzing the compiled machine code, and producing extensive proofs. An independent verification program called Rocq automatically checks those proofs, and according to Anthropic, the process needs almost no human reviewers. The researchers call it "fully autonomous" proof generation, though the tools and formal foundations were built by humans at Theorem. Ad
While generating proofs, Claude ran into hundreds of bugs and was allowed to fix them itself. Many would have slipped past conventional testing because they only show up under very specific conditions, like unusually large input files or a particular sequence of accesses, the researchers say.
During an effort to verify a widely used PDF reader, for example, the team found as many security bugs in one week as are typically reported for that software in an entire year. In another application, Claude caught a logical error that had gone undetected for over a decade. Even when a complete proof ultimately fails, Anthropic says, the attempt still surfaces real bugs. Ad
Anthropic acknowledges that "formally verified" doesn't mean "error-free." The proofs only hold under strict conditions: a specific processor architecture, single-threaded programs, and inputs under 64 MB. In practice, these libraries run on different hardware and in different configurations.
The compute cost is steep, with individual proofs running up hundreds of millions of tokens. Anthropic doesn't report total project costs. But if AI can verify its own code, developers can trust AI-generated software more and spend less time reviewing it. That saves costs not just on verification but on the entire coding process. A smaller test run also showed that proofs are reusable, and newer models are getting more efficient: Opus 5.5 solves half the proofs with about 40 percent fewer tokens than Opus 5. Ad
The project strengthens the case for software automation. If AI can write code and guarantee its correctness under defined conditions, the question shifts from "Can AI program?" to "Can AI prove that the code it writes is safe?" If the answer is yes, the consequences could go well beyond today's coding tools. Ad
Case in point: Anthropic expects formal verification with AI will soon become as practical as standard testing, and Theorem's roadmap already targets critical infrastructure like glibc, OpenSSL, and cURL.
Subscribe to THE DECODER for ad-free reading, a weekly AI newsletter, our exclusive "AI Radar" frontier report six times a year, full archive access, and access to our comment section.