Una prova formal és un argument que un programa verificador pot comprovar mecànicament, sense fiar-se de qui l'ha escrit. Fer-ne per a programes reals és tan car que gairebé només es fa en sistemes crítics. Anthropic, amb l'empresa Theorem, ha provat si Claude pot abaratir-ho.
El mètode parteix de les proves de fuzzing de l'OSS-Fuzz de Google, que llancen entrades aleatòries contra una biblioteca. Es compila la biblioteca a RISC-V, se'n converteix la prova en una especificació («aquest programa no es bloqueja amb cap entrada de menys de 64 MB») i Claude escriu en Rocq la demostració que l'especificació es compleix. El comprovador de Rocq la valida. Quan la prova s'encalla perquè hi ha un error, Claude el corregeix i ho torna a demostrar. L'empresa compta 123 biblioteques i 239 punts d'entrada, centenars d'errors trobats i unes 180 milions de línies de prova en total; una de sola en pot tenir uns 600.000. Entre els errors hi ha un desbordament d'un comptador en un descompressor, una lectura fora de límits en un descodificador d'imatges i una vulnerabilitat ja coneguda de libexpat.
Segons Anthropic, el cost es nota: una prova pot consumir centenars de milions de *tokens* (unitats de text que processa el model), tot i que Opus 5.5 n'hauria gastat un 40% menys que Opus 5 en 36 tasques petites, i compartir l'espai de treball entre proves n'estalvia un 17%. L'empresa afegeix altres casos, com un intèrpret de Python escrit en Rust que coincideix amb CPython en el 99,95% d'1,7 milions de programes aleatoris.
Els límits són importants i la mateixa empresa els enumera. Les proves valen per a binaris RISC-V estàtics i d'un sol fil amb Linux i musl, no per a les configuracions x86 i ARM amb glibc que usa la majoria de gent. No tots els punts d'entrada s'han verificat, un usuari que faci servir mal la biblioteca encara pot corrompre la memòria, i cal fiar-se del comprovador, dels models de RISC-V i Linux i del maquinari. És un informe de l'empresa, no un article revisat per parells.