Bewiesen statt getestet: KI rechnet Software jetzt nach. Was das für Ihre Produkte heißt

TL;DR. Am 22. Oktober haben Anthropic und die Firma Theorem gezeigt, dass Claude Software nicht nur testen, sondern mathematisch nachrechnen kann. Für 123 verbreitete Open-Source-Bibliotheken liegt jetzt ein maschinell geprüfter Beweis vor, dass bestimmte Programmteile bei keiner Eingabe unter 64 MB abstürzen. Unterwegs kamen Hunderte Fehler ans Licht, einer davon älter als zehn Jahre. Der Beweis gilt allerdings für eine Testumgebung, nicht für die Rechner, auf denen Ihre Software läuft. Formale Beweise werden bezahlbar. Wer heute Software testet, sollte die Tests so anlegen, dass man sie morgen beweisen kann.

Was neu ist: Beweis statt Stichprobe

Sicherheitskritische Bibliotheken werden heute vor allem mit Zufallstests geprüft. Beim sogenannten Fuzzing wirft ein Programm Millionen zufälliger Eingaben auf den Code und wartet auf einen Absturz. Googles Projekt OSS-Fuzz macht das für 1.381 Open-Source-Projekte. Das bleibt eine Stichprobe: Was die Tests nicht treffen, bleibt unentdeckt.

Anthropics Frontier Red Team beschreibt im Beitrag vom 22. Oktober den nächsten Schritt. Claude hat aus vorhandenen Fuzz-Tests formale Aussagen gemacht, etwa: Dieses Programm stürzt bei keiner Eingabe unter 64 MB ab. Dann hat es diese Aussagen bewiesen, und zwar für das fertig übersetzte Programm, nicht nur für den Quelltext. Ein unabhängiges Prüfprogramm namens Rocq kontrolliert jeden Schritt. Nach wenigen Wochen standen 239 Einstiegspunkte in 123 Bibliotheken, zusammen rund 180 Millionen Zeilen Beweis. Auf dem Weg fand Claude Hunderte Fehler, die trotz Billionen Testläufen jahrelang unentdeckt geblieben waren, und behob sie. Ein Logikfehler steckte seit mehr als zehn Jahren im Code.

Wie groß der Unterschied ist, zeigt ein kleiner Versuch aus dem Anhang. Das Team baute absichtlich sieben Fehler in einen Python-Interpreter ein, den Claude geschrieben und bewiesen hatte. Fünf davon überstanden die Zufallstests. Alle sieben brachen den Beweis.

Warum das bisher kaum jemand gemacht hat

Formale Beweise gibt es seit Jahrzehnten, etwa für Flugsteuerungen. Sie waren aber so aufwendig, dass sie fast nur dort vorkamen. Der Aufwand ist auch jetzt riesig, nur trägt ihn die Maschine. Für den 391 Zeilen langen Parser der Bibliothek cJSON schrieb Claude einen Beweis mit 630.000 Zeilen. Nur etwa ein Zehntel davon betrifft cJSON selbst. Der Rest beweist Startcode, Speicherverwaltung und Prüfwerkzeuge gleich mit. Insgesamt schrieb Claude rund eine Milliarde Zeilen, davon landeten 180 Millionen in Beweisen, die die Prüfung bestanden.

Ein einzelner Beweis braucht laut Anthropic Hunderte Millionen Token. Einen Preis nennt der Beitrag nicht. Die Prüfung eines fertigen Beweises dauert 30 Minuten bis mehrere Stunden Rechenzeit. Die Kurve zeigt aber nach unten: Opus 5.5 löst die Hälfte von 36 Beweisaufgaben mit rund 40 % weniger Token als Opus 5. Arbeiten mehrere Agenten in einem gemeinsamen Beweisraum, sparen sie weitere 17 %.

Der Haken

• Bewiesen für eine Testmaschine, nicht für Ihre Server. Die Beweise gelten für einfädige, statisch gebaute Programme auf der Prozessorarchitektur RISC-V mit der C-Bibliothek musl. Die meisten Server und Rechner laufen auf x86 oder ARM mit glibc.
• Kein Absturz heißt nicht richtig. Bewiesen ist, dass bestimmte Fehlerarten nicht auftreten. Ein falsches Ergebnis schließt das nicht aus. Anthropic schreibt selbst, formal verifiziert heiße nicht fehlerfrei. In der Diskussion auf Hacker News (442 Punkte) war das der häufigste Einwand: Ein Beweis zeigt nur, was in der Aussage steht.
• Die KI könnte schummeln. Claude hätte ein Programm so ändern können, dass es sich leicht beweisen lässt. Das Team hat solche Änderungen bestraft, protokolliert und nachgeprüft.
• Offen, ob es mitwächst. Im Anhang räumt das Team ein, dass andere Projekte mit diesem ausführlichen Beweisstil an eine Komplexitätswand gestoßen sind. Größere Programme brauchen vermutlich bessere Bausteine.
• Öffentlich prüfbar ist erst ein Teil. Im Archiv von Theorem liegen bisher Beweise für 25 Bibliotheken. Beweise, die noch nicht behobene Fehler verraten könnten, hält Anthropic zurück.

Unsere Auswertung: Wo stehen Bibliotheken aus der Industrie?

Theorem hat zum Start ein öffentliches Verzeichnis veröffentlicht. Es formuliert für 427 der 1.381 OSS-Fuzz-Projekte prüfbare Aussagen, insgesamt 20.164. Bewiesen sind davon 138, also 0,7 %. Wir haben am 24. Oktober nachgesehen, wie es um Bibliotheken steht, die in Maschinen, Anlagen und Netzwerken stecken.

Für OPC UA, den wichtigsten Standard für den Datenaustausch in der Fabrik, stehen 224 Aussagen bereit, keine davon ist bewiesen. Beim Energietechnik-Standard IEC 61850 sind es 116, ebenfalls ohne Beweis. Modbus lässt sich mit dem Modell noch gar nicht beschreiben. Bei OpenSSL sind 12 von 442 Aussagen bewiesen. Die Werkzeuge liegen also bereit, die Arbeit an der Industrie-Software fängt gerade erst an.

Was das für den Mittelstand heißt

Die meisten Mittelständler schreiben keine Kompressions- oder Verschlüsselungsbibliotheken. Sie bauen sie aber ein, in Maschinensteuerungen, Gateways, Webportale und Apps. Seit dem 11. September 2026 müssen Hersteller solcher Produkte nach dem Cyber Resilience Act aktiv ausgenutzte Schwachstellen binnen 24 Stunden melden. Ab Dezember 2027 gelten die übrigen Pflichten. Eine Fehlerart, die vor der Auslieferung bewiesen ausgeschlossen ist, führt später zu keiner Meldung.

Wichtig ist der Weg, den Anthropic gewählt hat: Jeder Beweis begann bei einem vorhandenen Fuzz-Test. Wer heute keine Tests hat, hat morgen nichts, was sich beweisen lässt. Anthropic erwartet, dass formale Beweise bald für fast jede Software so praktisch werden wie Fuzzing heute. Ob das so schnell geht, ist offen. Die Richtung ist es nicht.

Was Sie jetzt tun sollten

1. Wissen, was drinsteckt. Führen Sie für jedes Produkt mit Software eine Stückliste der Bibliotheken (SBOM). Der Cyber Resilience Act verlangt sie ohnehin.
2. Updates einspielen. Die gefundenen Fehler werden in den Bibliotheken selbst behoben. Bei Ihnen kommen die Korrekturen nur an, wenn Sie aktualisieren.
3. Parser zuerst testen. Programmteile, die Dateien oder Netzwerkdaten von außen lesen, sind das Einfallstor. Geben Sie ihnen Fuzz-Tests. Das ist heute gute Praxis und morgen die Voraussetzung für einen Beweis.
4. Lieferanten genau fragen. Wenn ein Anbieter „formal verifiziert“ verspricht: Was genau ist bewiesen, für welche Plattform, und was muss man dabei glauben?
5. Tests nicht abschaffen. Ein Beweis deckt nur ab, was in der Aussage steht. Für alles andere bleiben Tests nötig.

Formale Beweise waren bisher Handarbeit für wenige Fachleute. Jetzt werden sie zum Rechenauftrag, noch teuer und eng begrenzt, aber mit sinkenden Kosten. Wenn Sie wissen möchten, welche Bibliotheken in Ihren Produkten stecken und wo Tests fehlen, schauen wir gern gemeinsam darauf.