Bewiesen wurde Speichersicherheit: Die Programme enden laut Anthropic bei jeder Eingabe unter 64 MB normal, ohne Speicherfehler oder fehlschlagende Zusicherungen. Die Annahmen sind eng – ein einzelner Thread, ein statisch gelinktes Programm für RISC-V-Prozessoren unter Linux mit festem Speicherbudget. Geprüft wurde der Maschinencode, nicht der Quelltext, und nicht jeder Einstiegspunkt einer Bibliothek. Ein typischer Beweis umfasst rund 600.000 Zeilen in der Beweissprache Rocq, deren Prüfprogramm ihn maschinell kontrolliert.
Unterwegs fand Claude nach Anthropics Angaben Hunderte Fehler, darunter einen Logikfehler, der mehr als zehn Jahre unentdeckt geblieben war. Beim Versuch, einen verbreiteten PDF-Reader zu verifizieren, kamen in einer Woche so viele Sicherheitslücken zusammen, wie sonst in einem Jahr gemeldet werden.
Die größte Hürde bleibt der Aufwand. Agenten, die auf einen gemeinsamen Vorrat bereits bewiesener Bausteine zugreifen konnten, brauchten laut Anthropic 17 Prozent weniger Tokens. Theorem misst in einem eigenen Test, dass sich die Verifikationsgeschwindigkeit von sieben zwischen Mai und September 2026 erschienenen Modellen von Anthropic und OpenAI etwa alle zwei Monate verdoppelte.
Einen Teil der Beweise hat Theorem unter MIT-Lizenz auf GitHub veröffentlicht, zusammen mit den Modellen der RISC-V- und Linux-Semantik, auf denen sie aufbauen. Theorem bietet an, dieselbe Pipeline für weitere Open-Source-Projekte laufen zu lassen.