Il 22 ottobre il Frontier Red Team di Anthropic, insieme a Theorem, ha pubblicato i risultati di un lavoro in cui Claude ha scritto dimostrazioni formali di proprietà di sicurezza nel codice compilato di 123 librerie open source. Il verificatore di prove Rocq ha controllato ogni dimostrazione. L’impresa ha richiesto alcune settimane e ha coperto 239 punti di ingresso, cioè i test di fuzzing che il progetto OSS-Fuzz di Google mantiene per quelle librerie.
Che cosa è stato dimostrato
Ogni punto di ingresso del fuzzing è diventato una specifica: per qualsiasi input inferiore a 64 MB, il programma resta entro i confini della memoria e rispetta le proprie asserzioni. Gli errori esclusi sono quelli di sicurezza della memoria e le asserzioni fallite. Le prove riguardano il codice macchina RISC-V prodotto dalla compilazione, e ciò che viene dimostrato è dunque il binario eseguibile.
Le dimensioni sono quelle di un lavoro industriale. In totale le prove Rocq sfiorano i 180 milioni di righe, con una prova tipica di circa 600.000 righe, su binari la cui lunghezza mediana è di 18.000 istruzioni. Anthropic precisa che una singola prova può richiedere centinaia di milioni di token.
La catena di prova
Claude scrive la prova, il nucleo di Rocq la controlla contro la specifica. La divisione dei compiti è il punto centrale: il modello può imboccare molte strade sbagliate, e l’errore resta innocuo perché il verificatore respinge ogni passaggio scorretto. Quando una dimostrazione fa emergere un bug, Claude corregge il codice, rigenera la specifica e rifà la prova.
Il metodo ha un rischio tipico, il reward hacking: il modello potrebbe rendere dimostrabile un teorema modificando il programma in modo banale. Anthropic ha penalizzato le correzioni che cambiano il comportamento, ha premiato quelle minime e ha registrato e controllato ogni patch.
Che cosa è emerso
Il conteggio esatto dei bug manca: Anthropic parla di “centinaia”. Gli esempi descritti mostrano quanto siano rari i percorsi che il fuzzing fatica a raggiungere:
- un decompressore con un contatore in underflow che provoca una scrittura fuori dai limiti, innescata solo da input attorno a 20 MB con una disposizione particolare;
- un decodificatore di immagini con una lettura fuori dai limiti, che richiede un input da 64 MB e oltre 2 GB di memoria;
- libexpat, dove la prova ha riscoperto la CVE-2026-56132, attivata da input con annidamento profondo;
- un interprete Python scritto in Rust, con un bug logico latente da oltre dieci anni e un confronto su 1,7 milioni di programmi casuali che ha dato il 99,95 % di risultati identici a CPython.
Su zlib la specifica deriva dalla RFC 1950 ed è stata dimostrata sul binario x86 della versione inclusa nel kernel Linux. In una mezza dozzina di librerie sono emersi soltanto difetti minori e inutilizzabili per un attacco. Per un lettore di PDF il gruppo ha segnalato in una settimana tante falle di sicurezza quante se ne ricevono di norma in un anno.
I confini dichiarati
Anthropic ricorda che “verificato formalmente” equivale a una garanzia sulla specifica, e la corrispondenza fra specifica e realtà resta fuori dalla portata del verificatore. Il rapporto elenca quattro limiti:
- Piattaforma. Le prove valgono per programmi eseguiti come binario statico a singolo thread, con memoria fissa, su CPU RISC-V sotto Linux e libreria musl. Gli ambienti più diffusi, x86 e ARM con glibc dinamica, restano fuori.
- Perimetro. AddressSanitizer individua soltanto una parte dei bug di memoria, i punti di ingresso verificati sono un sottoinsieme, il codice morto è escluso e un chiamante può impiegare la libreria in modo scorretto.
- Base fiduciaria. Restano da credere la semantica di RISC-V e di Linux, gli enunciati dei teoremi e il verificatore Rocq, che a sua volta si appoggia su hardware, sistema operativo e compilatore OCaml.
- Costo. Centinaia di milioni di token per prova pongono un tetto alla diffusione, almeno finché i prezzi restano quelli attuali.
Anthropic rilascia un sottoinsieme delle prove, le semantiche affidabili e le specifiche per i test di fuzzing ancora da dimostrare. Theorem offre la pipeline ad altri progetti open source e ha pubblicato una skill per Claude.
Perché conta
Finora la verifica formale era appannaggio di codice piccolo e critico, perché scrivere le prove richiedeva anni di lavoro di specialisti. Qui il costo si converte in token e in settimane di calcolo, mentre il giudizio finale resta a un componente piccolo, deterministico e controllabile. Lo schema vale oltre il caso di specie: un modello generativo propone, un verificatore indipendente decide, e la delega regge nella misura in cui il controllo costa meno del compito.
Il contesto è quello ricostruito nel deep del 22 ottobre di questa sala stampa sul caso PHP2Shell, dove falle critiche scoperte con l’IA hanno messo sotto pressione i tempi dei manutentori. La stessa capacità che cerca vulnerabilità può dimostrare l’assenza di intere classi di difetti, entro la specifica scelta. Per chi acquista o integra componenti open source, le domande utili al fornitore sono tre: quale proprietà è stata dimostrata, su quale piattaforma e con quale base fiduciaria.
Quel che resta da decidere
Il primo nodo è economico: se il costo per prova scende abbastanza da entrare nei cicli di rilascio ordinari, la verifica formale smette di essere un lavoro per progetti eccezionali. Il secondo è editoriale: la specifica è la parte che il verificatore lascia al giudizio umano, e chi la scrive decide che cosa significhi “sicuro”. Resta da vedere se l’audit delle specifiche diventi il nuovo mestiere della sicurezza del software, e chi lo eserciterà.
Fonti
- “LLMs are making formal software verification feasible at a much larger scale” — Anthropic Research, 22 ottobre 2026
- OSS-Fuzz, il servizio di fuzzing continuo per il software open source — Google
- Rocq Prover, l’assistente di dimostrazione impiegato per il controllo delle prove — Rocq
- Theorem, collaboratore del lavoro e autore della pipeline di verifica — Theorem
- Deep del 22 ottobre 2026 di questa sala stampa sul caso PHP2Shell