La maggior parte del software è piena di bug. Questo lo sappiamo. Quello che forse non sapevamo è che gli LLM possono ora trovarli — e sfruttarli — con una facilità imbarazzante. Le difese standard non bastano più: servono modi per dimostrare matematicamente che il codice è pulito. La verifica formale poteva farlo, certo, ma richiedeva anni di lavoro da parte di esperti. Roba da progetti spaziali o avionica critica, non certo per la libreria open source che usate ogni giorno.
Anthropic, in collaborazione con Theorem, ha dimostrato che questo limite non esiste più. Claude ha prodotto prove formali su larga scala, dimostrando proprietà di sicurezza a livello di codice assembly (RISC-V) per oltre 100 librerie open source. Primo caso al mondo — per quanto ne sappiamo — di verifica formale assistita da AI applicata a software di produzione a livello assembly.
Quando i test non bastano
Anche il software più testato contiene bug. Il kernel Linux — girato su miliardi di dispositivi, sottoposto a test infiniti — ha visto oltre 1.000 vulnerabilità segnalate di recente. E i modelli frontier stanno diventando sempre più bravi a concatenare bug apparentemente innocui in exploit critici. Servono tecniche che trovino tutti i bug, li correggano, e poi dimostrino che non ce ne sono altri.
La verifica formale è una di queste tecniche. Si traduce il codice in un modello matematico e si prova che rispetta sempre certe regole di sicurezza. Se la prova fallisce, c’è un bug che viola una regola — e la natura del fallimento suggerisce dove sia. Ripeti il processo fino a ottenere la prova che il codice è pulito.
Il problema: non è facile. Le prove possono essere molte volte più grandi del codice originale. Il kernel seL4, per esempio: due anni-persona per implementarlo, 20 anni-persona per verificarlo formalmente. Ecco perché finora la verifica formale era riservata al codice davvero mission-critical, tipo quello dell’Airbus.
Da test a prove: trasformare il fuzzing in matematica
Per dimostrare che un pezzo di software è corretto, serve prima definire cosa significhi ‘corretto’. È la specifica. Per alcuni programmi è chiaro: un decoder PNG prende byte e restituisce un’immagine secondo RFC 2083. Ma per la maggior parte del software? Cosa significa che un editor di testo è ‘corretto’?
Anthropic ha aggirato il problema convertendo le suite di test esistenti in specifiche, codificando la regola ‘questa suite di test passa sempre’, usando un modello generale di cosa significhi eseguire un binario RISC-V compilato su Linux. Storicamente, dimostrare queste specifiche era intrattabile. Troppe istruzioni assembly, troppi comportamenti possibili, prove enormi.
Qui entrano gli LLM. Macinare milioni di righe di codice alla ricerca di un obiettivo ben definito è esattamente il tipo di compito in cui eccellono.
Il progetto è partito dai fuzz test. Gli sviluppatori scrivono un punto di ingresso che accetta input: qualsiasi input che causi un crash è un bug. Il fuzzer genera quantità enormi di input semi-casuali per trovare bug. Più a lungo gira, più bug trova. Ma è un processo di forza bruta: nessuna garanzia di testare ogni possibile percorso, non importa quanti input provi.
Anthropic ha trasformato il fuzz test in una specifica definita sulle istruzioni RISC-V compilate. La specifica dice: ‘il fuzz test non va mai in crash per nessun input sotto i 64 MB’. Se Claude riesce a dimostrarlo, il fuzz test diventa superfluo: non troverà mai bug.
L’hanno fatto per centinaia di progetti in OSS-Fuzz di Google, che fornisce fuzzing continuo a progetti open source qualificati. OSS-Fuzz contiene migliaia di punti di ingresso scritti dagli sviluppatori, strumentati con AddressSanitizer (ASan) — che fa crashare il programma ogni volta che la memoria viene acceduta in modo improprio. Una delle principali cause di vulnerabilità software.
I numeri: 239 prove, 180 milioni di righe, bug nascosti da un decennio
Nell’arco di poche settimane, Claude ha corretto i bug trovati e poi dimostrato l’assenza di crash su qualsiasi input (fino a 64 MB) per 239 punti di ingresso attraverso 123 librerie OSS-Fuzz diverse. Le prove operano sulle istruzioni RISC-V compilate — binari eseguibili, non codice sorgente — e comprendono circa 180 milioni di righe di Rocq. Una prova tipica: 600.000 righe per fornire garanzie di sicurezza su binari con una lunghezza mediana di 18.000 istruzioni RISC-V.
600.000 righe di prova per 18.000 istruzioni. Ecco perché nessuno lo faceva prima.
Queste prove assumono che il programma giri come binario statico single-thread con budget di memoria fisso su CPU RISC-V con Linux. Espandere lo scope è possibile — serve standardizzare semantiche per più architetture assembly e processi OS.
Ma c’è un vantaggio collaterale enorme: nel processo di tentare queste prove, Claude ha trovato centinaia di bug. Molti dei quali un fuzzer non avrebbe mai trovato. I fuzzer tipicamente mutano input piccoli, cappati a 1 MB, guidati dalla code coverage. Claude invece ha trovato un counter underflow in un decompressore che si manifestava solo su input di circa 20 MB con un layout specifico raro. Un out-of-bounds read in un decoder di immagini che richiedeva un input da 64 MB e oltre 2 GB di memoria. Un altro out-of-bounds read che necessitava di una sequenza particolare di chiamate attraverso due handle allo stesso file. E una riscoperta di CVE-2026-56132 in libexpat, che richiedeva input profondamente annidato.
Claude ha trovato anche bug logici che non causano mai crash. Durante la prova di memory safety di una libreria, ha notato che una funzionalità per limitare quali file un’applicazione può caricare non viene sempre applicata.
Alcuni di questi bug erano latenti da oltre un decennio. Nonostante — e cito testualmente — ‘trilioni di esecuzioni di test’.
Oltre la memory safety: dimostrare proprietà di alto livello
Dimostrare che un fuzz test non ha più crash da trovare è più significativo di quanto sembri. I fuzz test nel codice reale spesso testano violazioni di proprietà ad alto livello significative: roundtripping encode-decode, idempotenza, leggi algebriche, testing differenziale, auto-consistenza, equivalenza a implementazioni di riferimento.
Esempio: un fuzz test per l’algoritmo di compressione LZO asserisce che se comprimi un input e poi lo decomprimi, il risultato è uguale all’originale. Se la proprietà non vale, il programma crasha. Dimostrare che il test non crasha mai equivale a dimostrare la proprietà stessa.
A volte accade anche quando le proprietà non sono direttamente specificate dallo sviluppatore. Per completare la prova OSS-Fuzz per cpp-httplib, Claude ha dovuto escludere la possibilità di stack overflow dovuto a troppa ricorsione nel distruttore di std::set. La profondità di ricorsione è limitata dalla profondità massima dell’albero, quindi Claude ha dovuto dimostrare — su machine code — che l’algoritmo di ribilanciamento red-black tree di libc++ mantiene la profondità dell’albero logaritmicamente limitata.
Su machine code. Ci pensate?
Altri esperimenti: da zlib a un interprete Python in Rust
Anthropic ha chiesto a Claude di scrivere una specifica formale di RFC 1950, il documento tecnico che definisce il formato file di compressione zlib, e poi di dimostrare che l’implementazione zlib nel kernel Linux implementa correttamente quella specifica. A livello binario, questa volta su x86, usando semantiche formali x86 generate da Claude e pesantemente testate.
Hanno ripetuto il processo per mezza dozzina di altre librerie ampiamente usate. Durante il percorso, hanno trovato alcuni bug minori non sfruttabili in casi limite, ora in processo di segnalazione upstream. Due conclusioni: questi codebase estremamente testati sono già quasi completamente corretti, ed è possibile dimostrare proprietà di correttezza end-to-end su codebase reali esistenti.
In un altro esperimento, Claude ha sviluppato un interprete per un ampio sottoinsieme di Python in Rust e ha dimostrato, usando Verus, che aderisce alle semantiche CPython delineate in un paper accademico. Hanno poi misurato empiricamente l’aderenza al comportamento di CPython eseguendo oltre 1,7 milioni di programmi Python generati casualmente: comportamento identico a CPython nel 99,95% dei test.
Hanno anche trovato problemi in diverse applicazioni ampiamente usate tramite tentativi di verifica formale di proprietà di sicurezza semplici. In una di esse, hanno scoperto un bug logico precedentemente sconosciuto latente da oltre un decennio. Durante uno sforzo per verificare un lettore PDF ampiamente usato, hanno trovato in una settimana tanti bug di sicurezza quanti ne vengono tipicamente segnalati in un anno.
Il costo sta crollando (e le prove si possono riutilizzare)
Una limitazione chiave della verifica formale assistita da LLM è che le prove possono richiedere centinaia di milioni di token. L’efficienza è critica se l’obiettivo è rendere questi metodi disponibili all’intero ecosistema software. Ci sono ragioni solide per aspettarsi miglioramenti.
Opus 5.5 dimostra metà di 36 task di verifica costruiti da codice OSS-Fuzz reale con circa il 40% in meno di token rispetto a Opus 5. Il trend dovrebbe continuare man mano che i modelli vengono addestrati su task di verifica lunghi.
Le prove, come il software, sono costruite ricorsivamente da prove più piccole — e più piccole sono, più tendono a essere riutilizzabili. Quando gli agenti lavorano separatamente, spesso duplicano molto sforzo. Anthropic ha lasciato che gli agenti copiassero le prove degli altri mentre lavoravano sui propri obiettivi. Con accesso a questo workspace condiviso, gli agenti hanno usato il 17% in meno di token rispetto a quando lavoravano da soli.
Lo stesso fenomeno è emerso su larga scala durante lo sforzo di prova OSS-Fuzz. La maggior parte di una prova riguarda codice che ogni programma contiene — in particolare inizializzazione del C runtime e AddressSanitizer — quindi programmi molto diversi finiscono con prove significativamente sovrapposte. I team di agenti ne hanno approfittato copiando la prova finita di un altro team e adattandola al proprio programma.
Questa riutilizzabilità è come Mathlib, una libreria condivisa di matematica formale in Lean, è cresciuta fino a quasi 300.000 teoremi inviati da oltre 700 contributori: ogni nuova prova costruisce sul corpo di lavoro esistente.
Limitazioni: ‘Verificato formalmente’ non significa ‘bug-free’
Nella pratica, la verifica formale a volte dimostra meno sulla sicurezza del codice di quanto vorremmo. Claude può scrivere una prova che mostra che il comportamento di un programma compilato soddisfa i requisiti di una specifica formale, verificata da un proof checker esterno. Ma un proof checker non può dirvi se la vostra specifica corrisponde alla realtà.
Per corrispondere alla realtà, la specifica deve modellare correttamente tutto sulla macchina reale su cui gira il programma verificato, inclusi CPU e sistema operativo. Quando i bug appaiono in codice verificato, è perché la specifica, o le semantiche assunte della macchina, differiscono dalla realtà.
Le prove di Anthropic riguardano binari RISC-V statici single-thread linkati contro musl libc. Ma la maggior parte delle persone esegue queste librerie su x86 o ARM e le linka dinamicamente contro glibc. Per chiudere questo gap servirebbero modelli di sistema più vicini ai sistemi effettivamente deployati.
Hanno dimostrato che un crash non si innesca mai per nessun input sotto 64 MB su molti punti di ingresso di fuzzing in Google OSS-Fuzz, inclusi crash ASan. Ma ASan non rileva tutti i bug di memory safety, e non hanno verificato tutti i punti di ingresso per ogni libreria. Anche se l’avessero fatto, l’intera libreria non sarebbe coperta, specialmente se c’è dead code. Programmi reali potrebbero inoltre usare male la libreria, portando a corruzione di memoria nel chiamante.
Man mano che impariamo a sfruttare gli LLM per i metodi formali, e man mano che i modelli migliorano, queste limitazioni diventeranno trattabili.
La traiettoria è chiara
La verifica formale, storicamente pratica solo per garanzie su misura nel codice più safety-critical, sarà presto pratica quanto il fuzzing lo è oggi per quasi tutto il software di produzione. Come i tipi statici, i framework di testing e altri strumenti di correttezza, la verifica maturerà da ‘aggiunta posticcia’ a ‘integrata’, guidata non solo dagli LLM ma anche da innovazioni nel design dei linguaggi e nei workflow di sviluppo.
In un mondo dove gli LLM scansionano e trovano automaticamente sempre più vulnerabilità nel codice, servono processi che possano garantire proprietà di sicurezza. La verifica formale scalata via LLM è un approccio promettente per estendere queste garanzie a uno scope e una scala che prima erano irraggiungibili.
Anthropic ha pubblicato un subset di queste prove, le semantiche RISC-V e OS, e Theorem sta offrendo di eseguire la stessa pipeline per altri progetti open source. Sperimentate — specialmente se avete già provato con modelli meno capaci e non ha funzionato. Ora è diverso.
