Anthropic usa Claude per la verifica formale del codice: 239 funzioni dimostrate sicure

Il 22 ottobre 2026 Anthropic ha pubblicato una ricerca che cambia il modo in cui si può garantire la sicurezza del software. Il Frontier Red Team dell’azienda, insieme a Theorem, un collaboratore specializzato in metodi formali, ha usato Claude per scrivere dimostrazioni matematiche del fatto che alcune librerie open source non possono andare in crash. Non si parla di test che non trovano errori, ma di prove che un verificatore automatico controlla in modo meccanico. È un passaggio rilevante, perché finora la verifica formale è stata un lavoro rarissimo e costosissimo, riservato a pochi componenti davvero critici.

In sintesi: 239 punti di ingresso in 123 librerie, dimostrati sicuri su input fino a 64 MB, e centinaia di bug scovati lungo il percorso.

Che cosa ha fatto Anthropic con Claude

Secondo la ricerca pubblicata da Anthropic, l’obiettivo era dimostrare che il codice compilato non può bloccarsi in modi specifici: errori di memoria e asserzioni che falliscono. Il team ha lavorato su 123 librerie open source reali e, per ciascuna, ha chiesto a Claude di produrre una prova formale che gli eseguibili restano al sicuro per qualsiasi input in un intervallo definito. Anthropic la descrive come la prima iniziativa su larga scala in cui l’AI verifica formalmente software di produzione a livello di codice assembly.

Il punto di partenza è un’idea intelligente: non scrivere le specifiche da zero, ma ricavarle da qualcosa che gli sviluppatori hanno già.

Dai fuzz test alle specifiche formali

Molti progetti open source includono fuzz test, cioè programmi che bombardano una funzione con input generati per cercare crash. Il limite del fuzzing è noto: per quanto sia esteso, non può coprire ogni percorso possibile, quindi non dimostra mai l’assenza di bug. Anthropic ha preso ciascun fuzz test e lo ha trasformato in una specifica formale scritta sulle istruzioni RISC-V del programma compilato. La specifica afferma che quel punto di ingresso non va mai in crash per nessun input sotto i 64 MB. Il lavoro è partito dai punti di ingresso del programma OSS-Fuzz di Google, che raccoglie molti progetti C e C++ strumentati con AddressSanitizer, e poggia sui modelli formali di Theorem per il set di istruzioni RISC-V e per il comportamento dei processi Linux.

Il ruolo del verificatore Rocq

Qui entra in scena Claude. Il modello scrive le dimostrazioni e il proof checker Rocq le verifica in modo meccanico. Questo dettaglio è decisivo: i revisori umani non hanno dovuto leggere il codice delle prove, perché se il verificatore le accetta, sono corrette rispetto alla specifica. Quando un tentativo di prova portava alla luce un bug, Claude correggeva il codice, rigenerava la specifica e riprovava.

C’è anche una precauzione contro le scorciatoie. Anthropic ha penalizzato le modifiche non necessarie e ha registrato e controllato tutte le patch, per evitare il reward hacking, cioè il caso in cui un modello fa passare una prova alterando il programma invece di dimostrarne la correttezza.

I numeri della ricerca

Le dimensioni del lavoro sono impressionanti. Le dimostrazioni totalizzano circa 180 milioni di righe di Rocq, con una prova tipica da circa 600.000 righe che copre binari con una lunghezza mediana di 18.000 istruzioni RISC-V. L’intero sforzo su OSS-Fuzz ha richiesto qualche settimana. Alcune prove, ammette Anthropic, consumano centinaia di milioni di token, e per questo l’efficienza dei costi resta una questione centrale.

Sul fronte dei modelli, in un insieme di 36 piccoli compiti di verifica Opus 5.5 ne ha risolti la metà usando circa il 40% di token in meno rispetto a Opus 5. Gli spazi di lavoro condivisi tra agenti hanno ridotto il consumo di token del 17% rispetto ad agenti che lavorano da soli, e alcuni agenti sono riusciti in compiti in cui da soli avevano fallito.

Bug che il fuzzing non aveva visto

Il risultato più concreto riguarda gli errori scoperti. Durante i tentativi di prova sono emersi centinaia di bug sopravvissuti per anni ai test, fuzzing compreso. Tra gli esempi citati ci sono un underflow di un contatore in un decompressore, che causava una scrittura fuori dai limiti con input da circa 20 MB, e una lettura fuori dai limiti in un decodificatore di immagini, raggiungibile solo con un input da 64 MB e oltre 2 GB di memoria. Il team ha anche riscoperto una vulnerabilità di libexpat, identificata come CVE-2026-56132.

Sono proprio i casi che i test casuali faticano a raggiungere, e che una dimostrazione esaustiva intercetta per costruzione.

zlib, Python in Rust e un lettore PDF

Oltre alla campagna sulle 123 librerie, Anthropic racconta tre casi di studio. Nel primo, Claude ha scritto una specifica formale della RFC 1950 e ha dimostrato che l’implementazione di zlib del kernel Linux la rispetta a livello di binario x86, usando una semantica x86 generata dallo stesso Claude. Lo stesso procedimento, applicato a circa altre sei librerie molto usate, ha rivelato soltanto bug minori e non sfruttabili.

Nel secondo caso Claude ha costruito in Rust un ampio sottoinsieme di Python e ha usato Verus per dimostrare che ne segue la semantica di CPython. Su 1,7 milioni di programmi casuali, il comportamento coincideva con quello di CPython nel 99,95% dei casi.

Nel terzo, applicato a un lettore PDF, i tentativi di verifica su semplici proprietà di sicurezza hanno trovato in una settimana tanti bug quanti ne vengono di solito segnalati in un anno. Tra questi, un errore logico in un’applicazione molto diffusa, rimasto inosservato per oltre dieci anni.

I limiti: verificato non significa privo di bug

Anthropic è esplicita su un punto: formalmente verificato non vuol dire senza difetti. Una prova vale quanto la specifica e il modello della macchina su cui poggia, e i bug possono annidarsi nei componenti di cui ci si fida: la semantica di RISC-V e di Linux, gli enunciati dei teoremi, il verificatore Rocq, l’hardware, il sistema operativo e il compilatore OCaml.

Esiste poi un divario di modellazione. Le prove assumono un binario RISC-V statico, a thread singolo e con libc musl, mentre la maggior parte dei sistemi reali usa x86 o ARM con collegamento dinamico a glibc. C’è anche un divario di copertura: AddressSanitizer non intercetta ogni errore di memoria, non tutti i punti di ingresso sono stati verificati, e chi usa male una libreria può comunque causare corruzione di memoria, a meno di specificare anche gli obblighi del chiamante.

Anthropic si aspetta che questi limiti si riducano con il miglioramento dei modelli e dice che pubblicherà un sottoinsieme delle prove, le semantiche di riferimento e le specifiche dei fuzz test che non è riuscita a dimostrare.

Perché conta per sviluppatori e aziende

Il messaggio di fondo è che il costo della verifica formale sta scendendo, perché il lavoro più laborioso, scrivere prove lunghe centinaia di migliaia di righe, può essere delegato a un modello mentre la correttezza resta garantita da un verificatore deterministico. Se chi scrive la prova è un’AI, ma chi la controlla è un programma matematico, la fiducia non dipende dal modello.

Non è la prima volta che Claude si muove su terreni di rigore matematico e sicurezza. Se segui Claude e gli strumenti di Anthropic, ricorderai il lavoro in cui il modello ha svelato l’origine dei seed delle curve NIST, oppure quello in cui Claude progetta circuiti quantistici con molte meno porte. La verifica formale del software si inserisce in questa traiettoria: l’AI non soltanto scrive codice, ma comincia a dimostrarne le proprietà.

Per chi si occupa di sicurezza, il fuzzing resta utile, ma diventa il materiale grezzo per qualcosa di più forte. Per chi sviluppa librerie critiche, compressione, parsing di formati, decodifica di immagini, la prospettiva è avere garanzie che finora erano fuori budget.

Conclusioni

La ricerca di Anthropic non dice che il software è diventato a prova di bug, e lo stesso team lo ripete con chiarezza. Dice però che un modello può scrivere prove formali su scala industriale, che un verificatore le può controllare senza fidarsi di nessuno e che il risultato fa emergere errori nascosti da anni. Resta da vedere quanto i costi in token scenderanno e quanto i modelli formali copriranno architetture come x86 e ARM.

Se lavori con codice critico, tieni d’occhio le prove e le specifiche che Anthropic ha promesso di pubblicare e leggi con attenzione la fonte primaria. Seguici per i prossimi aggiornamenti su AI, sicurezza e sviluppo software.