Softwaretests zeigen, dass ein Programm in vielen geprüften Fällen funktioniert. Ein formaler Beweis kann für eine genau definierte Eigenschaft sehr viel stärker sein. Anthropic und Theorem haben Claude nun solche Beweise in ungewöhnlichem Maßstab schreiben lassen.
Quellen:
https://www.anthropic.com/research/formal-verification
https://github.com/theorem-labs/oss-verify-proofs
https://www.aiaffairs.com/technology/anthropic-theorem-claude-formal-verification-123-libraries/
🔎 Was ist passiert?
Claude erzeugte nach Angaben von Anthropic und Theorem rund 180 Millionen Zeilen Rocq-Beweiscode. Ein kleiner, vertrauenswürdiger Rocq-Kern prüfte anschließend mechanisch, ob die Beweise zu den vorgegebenen mathematischen Aussagen passen.
Für 239 Einstiegspunkte aus 123 Open-Source-Bibliotheken wurden No-Crash-Eigenschaften bewiesen. Die Programme waren als statische, einzelthreadige RISC-V-Binärdateien unter einem modellierten Linux-System dargestellt. Abgedeckt waren Eingaben unter 64 MB, modellierte Betriebssystemantworten und Speicherlayouts bei festem Speicherbudget.
Während der Arbeit fand Claude auch Fehler, die trotz sehr vieler vorheriger Fuzzing-Durchläufe unentdeckt geblieben waren. Ein Teil der Beweise, Spezifikationen sowie RISC-V- und Betriebssystemmodelle wurde öffentlich bereitgestellt.
⚖️ Der Realitätscheck
Ein maschinell geprüfter Beweis bedeutet hier nicht, dass 123 Bibliotheken vollständig fehlerfrei sind. Bewiesen wurde eine bestimmte Eigenschaft bestimmter kompilierter Einstiegspunkte unter bestimmten Annahmen. Fehler außerhalb dieser Spezifikation, andere Architekturen, Mehrthreadbetrieb, dynamische Bibliotheken oder unzutreffende Modelle bleiben möglich.
Vertrauen muss weiterhin in den Rocq-Prüfkern, die formalen RISC-V- und Linux-Modelle und vor allem die präzise formulierte Aussage gesetzt werden. Ein korrekt bewiesener, aber zu enger Satz kann wichtige Fehlverhalten unberührt lassen.
Außerdem ist nur eine Teilmenge öffentlich. Eine unabhängige vollständige Reproduktion des gesamten 123-Bibliotheken-Laufs liegt damit noch nicht vor. Die veröffentlichten Artefakte machen zumindest eine externe Prüfung des freigegebenen Teils möglich.
💡 Warum ist das interessant?
Formale Verifikation scheiterte im Alltag oft weniger an ihrer Logik als an ihrem enormen Arbeitsaufwand. Wenn Modelle den größten Teil des Beweiscodes erzeugen und ein kleiner Prüfer jeden Schritt kontrolliert, könnte die Methode von Spezialprojekten in breitere Softwareentwicklung wandern.
Das verschiebt die Rolle der Menschen: Sie müssen die richtige Sicherheitsfrage formulieren, Modelle und Annahmen kontrollieren und entscheiden, welche Garantien tatsächlich relevant sind. Claude ersetzt den Prüfkern nicht – es automatisiert vor allem die mühsame Suche nach einem Beweis, den der Prüfkern anschließend akzeptiert oder verwirft.
Schreibe einen Kommentar