Anthropic afferma che Claude ha dimostrato proprietà di sicurezza in 123 librerie

Il 22 ottobre 2026, Anthropic ha pubblicato una ricerca in cui riferisce che Claude ha prodotto prove formali verificate automaticamente di proprietà di sicurezza a livello di codice assembly RISC-V per 239 punti di ingresso dei test di fuzzing distribuiti in 123 librerie open source, nell’ambito di una collaborazione con Theorem.

Secondo Anthropic, Claude ha corretto i bug individuati e poi ha dimostrato che i programmi terminano sempre normalmente, senza generare errori di sicurezza della memoria né asserzioni non soddisfatte, per qualsiasi input inferiore a 64 MB e per ogni risposta modellata del sistema operativo Linux e layout di memoria. Le dimostrazioni presuppongono che il programma venga eseguito come binario statico a thread singolo, con un budget di memoria fisso, su una CPU RISC-V con Linux. Anthropic ha dichiarato che le dimostrazioni comprendono circa 180 milioni di righe di codice Rocq e che una dimostrazione tipica è composta da circa 600.000 righe per coprire binari con una lunghezza mediana di 18.000 istruzioni RISC-V. L’azienda ha affermato che, per quanto ne sa, si tratta del primo progetto su larga scala che utilizza l’IA per applicare la verifica formale a software di produzione a livello di codice assembly.

Una parte delle dimostrazioni, insieme alla semantica RISC-V e del sistema operativo su cui si basano, sarà pubblicata su GitHub. Anthropic ha dichiarato che renderà pubblici anche i componenti attendibili realizzati per il progetto che non erano già disponibili, le dimostrazioni complete per i test di fuzzing che non hanno richiesto correzioni e le specifiche dei test di fuzzing che non è riuscita a dimostrare, mentre non pubblicherà le dimostrazioni che potrebbero rivelare un bug non corretto.

Dai test di fuzzing alle dimostrazioni formali

Questo approccio converte il test di fuzzing già esistente e compilabile di ciascuna libreria in una specifica formale che codifica una regola: il test non va mai in crash con input inferiori a 64 MB. La specifica è definita sulle istruzioni RISC-V compilate, usando la semantica formale di Theorem per il set di istruzioni RISC-V e i processi Linux; il verificatore di dimostrazioni Rocq controlla poi ogni dimostrazione completata rispetto alla specifica. Anthropic afferma che, di conseguenza, gli sviluppatori devono fidarsi di soli tre componenti: i modelli formali di RISC-V e dei processi Linux, gli enunciati esatti dei teoremi e il verificatore Rocq stesso.

Anthropic ha dichiarato di aver applicato questo processo a centinaia di progetti dell’iniziativa OSS-Fuzz di Google, che offre test di fuzzing continui per i progetti open source idonei e strumenta automaticamente i programmi C e C++ con AddressSanitizer, uno strumento che provoca un crash del programma ogni volta che la memoria viene utilizzata in modo improprio. Un’appendice datata 22 ottobre 2026 illustra il teorema completo dimostrato: per tutti gli input inferiori a 64 MiB e tutti i layout di memoria, né il binario strumentato con ASan né quello non strumentato subiscono errori, interruzioni o comportamenti non modellati; entrambi producono inoltre tracce di lettura e scrittura, comportamenti all’uscita e stati finali del file system identici.

L’appendice afferma che, durante il progetto, Claude ha scritto circa un miliardo di righe di codice Rocq, di cui circa 180 milioni hanno superato il controllo del verificatore di dimostrazioni. Il punto di ingresso del parser di cJSON, composto da 391 righe, ha ricevuto una dimostrazione di 630.000 righe, mentre fftw3, con 51.000 righe collegate, ne ha ricevuta una di 480.000. Poiché Claude poteva correggere il codice prima di completare una dimostrazione, Anthropic ha dichiarato di aver penalizzato le correzioni, assegnato crediti aggiuntivi per la dimostrazione di quali input venissero modificati da una correzione e registrato e sottoposto a verifica le modifiche per scoraggiare la manipolazione del sistema di ricompense.

Bug individuati durante i tentativi di dimostrazione

Anthropic riferisce che i tentativi di dimostrazione hanno fatto emergere centinaia di bug, molti dei quali difficilmente individuabili con un fuzzer. Durante la dimostrazione relativa al punto di ingresso di una libreria, Claude ha individuato un underflow di un contatore in un decompressore, che causava una scrittura fuori dai limiti, ma solo con input di circa 20 MB e uno specifico layout raro. Tra le altre vulnerabilità individuate figurano una lettura fuori dai limiti in un decoder di immagini, che richiedeva un input di 64 MB e oltre 2 GB di memoria; una lettura fuori dai limiti che richiedeva una particolare sequenza di chiamate su due handle dello stesso file; e la nuova individuazione della CVE-2026-56132 in libexpat, che richiedeva un input profondamente annidato.

Claude ha inoltre individuato bug logici che non provocano mai un crash, tra cui una restrizione, non sempre applicata, sui file che un’applicazione può caricare. Anthropic ha dichiarato che i tentativi di verifica su diverse applicazioni critiche ampiamente utilizzate hanno portato alla scoperta di un bug logico precedentemente sconosciuto, rimasto latente per oltre un decennio; ha aggiunto che, durante un progetto di verifica di un lettore PDF molto diffuso, in una sola settimana ha trovato tanti bug di sicurezza quanti ne vengono segnalati in genere in un anno.

Altri esperimenti e risultati sull’efficienza

Oltre a OSS-Fuzz, Anthropic ha chiesto a Claude di redigere una specifica formale della RFC 1950, il documento tecnico che definisce il formato di compressione zlib, e di dimostrare poi che l’implementazione di zlib nel kernel Linux la rispetta correttamente. Claude ha dimostrato direttamente il binario compilato per x86, utilizzando la semantica formale del set di istruzioni x86 generata da Claude; Anthropic ha dichiarato di aver ripetuto il processo per altre sei librerie ampiamente utilizzate, individuando bug minori nei casi limite, non sfruttabili, che saranno segnalati ai manutentori dei progetti. L’azienda ha inoltre riferito che la generazione della semantica x86 ha permesso di identificare centinaia di errori nella documentazione di riferimento ufficiale e un numero minore di bug nell’hardware stesso, e che l’esecuzione passo-passo della semantica può avviare un ambiente utente Ubuntu su un kernel Linux.

In un altro esperimento, Claude ha realizzato in Rust un interprete per un ampio sottoinsieme di Python e ha dimostrato, usando lo strumento di verifica Verus, che rispetta la semantica di CPython descritta in un articolo accademico. L’appendice tecnica afferma che sono stati dimostrati tutti e 17 i livelli dell’interprete e che il teorema stabilisce che «ogni volta che l’interprete restituisce un risultato, quel risultato è quello prescritto dalla semantica formale». Anthropic ha dichiarato che i test empirici condotti su 1,7 milioni di programmi Python generati casualmente hanno rilevato un comportamento identico a quello di CPython nel 99,95% dei casi; dei sette bug inseriti deliberatamente, cinque sono sfuggiti ai test casuali, mentre tutti e sette hanno invalidato la dimostrazione.

Per misurare l’efficienza, Anthropic ha creato 36 piccoli compiti di verifica riducendo i punti d’ingresso di OSS-Fuzz reali. Ne sono risultati programmi composti da 283–2.491 istruzioni, con input limitati a 64 byte e AddressSanitizer sostituito da un ambiente di esecuzione «mini-ASan» di circa 100 istruzioni. Anthropic riferisce che Opus 5.5 dimostra la correttezza di metà dei compiti usando circa il 40% di token in meno rispetto a Opus 5. Anthropic riferisce inoltre che gli agenti autorizzati a copiare le dimostrazioni reciproche in un’area di lavoro condivisa hanno avuto bisogno del 17% di token in meno rispetto agli agenti che lavoravano da soli; alcuni sono riusciti nell’impresa dopo aver fallito in precedenza da soli, mentre gli agenti che lavoravano individualmente non sono riusciti a completare due delle dimostrazioni. L’azienda ha dichiarato che lo stesso effetto di riutilizzo si è manifestato su larga scala durante il lavoro su OSS-Fuzz, quando i gruppi di agenti hanno copiato dimostrazioni completate e le hanno adattate, poiché gran parte di ciascuna dimostrazione riguarda il codice di inizializzazione condiviso del runtime C e di AddressSanitizer.

Limiti dichiarati e programma OSS Verify

Anthropic precisa che le dimostrazioni non significano che le librerie siano prive di bug: quelli eventualmente rimasti potrebbero trovarsi nei componenti considerati affidabili o al di fuori dell’ambito delle dimostrazioni. Le dimostrazioni riguardano binari RISC-V statici e a thread singolo, collegati a musl libc, mentre la maggior parte degli utenti esegue queste librerie su x86 o ARM e le collega dinamicamente a glibc; inoltre, AddressSanitizer non rileva tutti i bug relativi alla sicurezza della memoria. L’azienda ha dichiarato di aspettarsi che questi limiti diventino gestibili con il miglioramento dei modelli.

Theorem offre gratuitamente la stessa pipeline ai progetti open source idonei tramite il programma OSS Verify. Per aderire, occorre inviare una pull request che aggiunga al repository del programma i file project.yaml, Dockerfile e build.sh. Theorem afferma di esaminare i progetti secondo criteri simili a quelli di OSS-Fuzz, dando priorità alle infrastrutture critiche ampiamente utilizzate. Secondo Theorem, i manutentori ricevono una dimostrazione in Rocq, verificata dal kernel di Rocq, che attesta che ciascun obiettivo di fuzzing non va in crash con alcun input fino a 64 MiB; i bug individuati durante il lavoro di dimostrazione vengono comunicati privatamente ai manutentori via e-mail, senza una scadenza per la divulgazione, e la produzione delle dimostrazioni può richiedere più giorni. La roadmap di Theorem punta a verificare l’intero ecosistema Nix, comprese infrastrutture critiche come glibc, OpenSSL e cURL.