Il 22 ottobre 2026 Anthropic ha pubblicato i risultati di un lavoro con Theorem: Claude ha generato prove formali di assenza di crash per 239 punti d’ingresso in 123 librerie Google OSS-Fuzz, e il kernel di Rocq le ha controllate. Il risultato riguarda input inferiori a 64 MB e un modello preciso di binario RISC-V e sistema Linux, non tutte le funzioni delle librerie.
Come Claude e Rocq trasformano i test in prove
La verifica formale consiste nel definire matematicamente una proprietà di un programma e dimostrare che il programma, secondo un modello specificato, la rispetta. Anthropic ha convertito test fuzz esistenti, cioè prove che eseguono il programma con input generati, in specifiche formali per binari RISC-V. Theorem ha fornito le semantiche delle istruzioni RISC-V e dei processi Linux usate nel modello.
Claude ha scritto il codice delle prove; il kernel di Rocq, il componente che controlla le dimostrazioni, ha verificato che derivassero dalle specifiche. Questo controllo stabilisce che la prova rispetta la proprietà formalizzata: non stabilisce, da solo, che la specifica descriva ogni comportamento che ci si aspetta dal software.
Che cosa coprono i 239 punti d’ingresso
Per ciascun punto verificato, la proprietà principale riguarda l’assenza di crash con input inferiori a 64 MB, secondo il binario e il sistema modellati. La verifica comprende gli errori di sicurezza della memoria e le asserzioni fallite rappresentati nella specifica.
Il modello assume un binario statico, single-thread e con un budget di memoria fisso, compilato per RISC-V e in esecuzione secondo le semantiche di Linux. Anthropic riferisce di aver verificato punti d’ingresso selezionati, non tutti quelli presenti nelle librerie; una prova su un punto d’ingresso non copre automaticamente ogni comportamento della libreria né il modo in cui un programma chiamante la usa.
I bug segnalati durante il lavoro
Anthropic riferisce che Claude ha corretto bug incontrati nel tentativo di dimostrare le proprietà, poi ha rigenerato le specifiche sul codice modificato. Tra gli esempi segnalati, un underflow del contatore di un decompressore provocava una scrittura fuori dai limiti con una rara configurazione di input di circa 20 MB. Un decoder di immagini presentava una lettura fuori dai limiti con un input di 64 MB e oltre 2 GB di memoria.
Il resoconto cita anche una lettura fuori dai limiti che richiedeva una particolare sequenza di chiamate attraverso due handle dello stesso file e la riscoperta della vulnerabilità CVE-2026-56132 in libexpat, con input annidati in profondità. Anthropic afferma di aver penalizzato le patch, chiesto prove sugli input modificati e registrato e sottoposto a controllo le modifiche per ridurre il rischio che le correzioni alterassero il comportamento atteso.
Dove finisce la garanzia
Una prova formale vale per la proprietà, gli input, il binario e il modello descritti dalla specifica. Il risultato non certifica ogni punto d’ingresso o ogni comportamento di una libreria: restano fuori dal perimetro anche il codice non raggiunto dai punti verificati e gli errori introdotti da chi chiama una libreria.
Conta anche il modello della macchina. La campagna principale riguarda programmi RISC-V statici e single-thread, mentre il comportamento di un sistema reale può dipendere dalla configurazione effettivamente usata. Anthropic osserva inoltre che AddressSanitizer, uno strumento che inserisce controlli nel codice C e C++ durante l’esecuzione, non rileva tutti i problemi di sicurezza della memoria.
Che cosa aggiunge il caso Python
In uno studio separato, Verus ha verificato tutti i 17 livelli di un interprete Python scritto in Rust rispetto alla semantica formale definita dal progetto. Il confronto con CPython è stato invece empirico: Anthropic riferisce una corrispondenza del 99,95% in oltre 1,7 milioni di programmi generati. Quel risultato misura il comportamento osservato in quei test, non dimostra l’equivalenza con CPython per ogni programma.
L’appendice distingue inoltre circa un miliardo di righe Rocq generate nei tentativi da circa 180 milioni di righe incluse nelle prove che hanno superato il controllo. Una prova completata tipica contava circa 600.000 righe distribuite in circa 1.400 file; il controllo richiedeva da 30 minuti a diverse ore di tempo CPU.
