Autore di immagini · divulgatore e formatore AI
180 milioni di righe, e nessuna è il programma 16 min di lettura
Intelligenza Artificiale ·

180 milioni di righe, e nessuna è il programma

Claude ha scritto le prove, una macchina le ha controllate su 123 librerie. Il numero misura la prova, non il software coperto.

📌 Abstract rapido. Il titolo che ha fatto il giro è “Claude scrive il codice e lo dimostra sicuro”. Letta la fonte originale, il quadro è più piccolo e più interessante: codice già esistente, una sola proprietà, nessuno strumento da provare oggi. In fondo trovi tre abitudini che puoi usare già stasera con gli script che ti fai scrivere dall’AI. Un avviso: le fonti principali sono di parte (Anthropic vende Claude, Theorem vende verifica) e non ho trovato commenti di esperti indipendenti. Te lo dico io, così non devi cercarlo tu.

Centottanta milioni di righe.

Quando ho letto il numero, ho pensato a un software enorme, controllato fino all’ultima riga da una macchina. È l’immagine che ti lascia il titolo con cui la notizia è circolata, quello di The Decoder del 23 ottobre 2026: “Claude now writes code and proves it safe automatically”. L’AI scrive il codice e lo dimostra sicuro. Fine dei bug.

Poi sono andato a leggere la fonte originale, e quei 180 milioni di righe non sono quello che pensi.

Non sono righe di software verificato. Sono righe di prova: il testo, scritto in un linguaggio per macchine, che serve a dimostrare che un pezzo di software si comporta in un certo modo. La fonte dice testualmente “about 180 million lines of Rocq” (Anthropic, 22 ottobre 2026). Rocq è lo strumento che le controlla (si chiamava Coq, prima).

Capire la differenza tra “righe di software” e “righe di prova” è il cuore di questo articolo. Perché da lì in poi tutto il resto si rimette a posto: che cosa è stato fatto, che cosa no, e che cosa ci puoi fare tu, che magari non hai mai aperto un editor di codice ma ti fai scrivere script e automazioni da Claude o da ChatGPT.

Cosa è stato annunciato davvero (e cosa no)

Il 22 ottobre 2026 il Frontier Red Team di Anthropic (il gruppo che mette alla prova i limiti dei modelli) ha pubblicato i risultati di un lavoro fatto insieme a Theorem, un’azienda che si occupa di verifica formale del software (Anthropic, 22 ottobre 2026).

Verifica formale vuol dire questo: invece di provare un programma con qualche esempio e sperare che vada, scrivi una dimostrazione, come in matematica, che vale per tutti i casi entro certi confini. Poi un controllore automatico (il “checker”) legge la dimostrazione riga per riga e dice se regge.

I numeri, dalla fonte: 239 punti di ingresso di test casuali in 123 librerie open source, in “a few weeks” di lavoro. Le prove le ha scritte Claude. Il checker Rocq le ha controllate (Anthropic).

Due traduzioni, così non resta nulla di oscuro:

  • Libreria open source: un pezzo di software pubblico e gratuito che altri programmi usano come mattone. Quella che apre un file compresso, quella che legge un’immagine, quella che interpreta un documento.
  • Test casuale (fuzz test): un metodo in cui bombardi il programma di input generati a caso, per vedere se qualcuno lo fa saltare.

Ora la parte che i titoli saltano. Il progetto principale, quello sulle 123 librerie, non ha scritto programmi nuovi e poi dimostrato che erano sicuri. Ha preso software che esisteva già, e ha dimostrato una cosa sola. Questa cosa sola la vediamo tra poco.

Quindi il titolo di The Decoder è più forte di ciò che la fonte primaria dimostra. Non lo dico per fare il pignolo: lo dico perché se sbagli la lettura qui, sbagli le decisioni dopo. Se credi che l’AI scriva codice “dimostrato sicuro”, smetti di controllare. E la fonte originale è la prima a dirti di non farlo.

I numeri, uno per uno

Facciamo l’esercizio che andrebbe fatto con ogni numero spettacolare.

180 milioni di righe. Sono righe della prova, come detto. Una prova tipica è lunga circa 600.000 righe. Il programma che dimostra, preso in versione già compilata per il processore (il binario), ha in mediana 18.000 istruzioni (Anthropic).

Metti in fila le due cose. Un programma piccolo, di qualche migliaio di istruzioni, e una dimostrazione lunga centinaia di migliaia di righe. È come se, per garantire che un ponte pedonale non cade in un certo scenario, servisse un fascicolo di calcoli grosso come un’enciclopedia. Il numero grande dice quanto è pesante la prova, non quanto software hai coperto.

Il costo. La fonte scrive che “the proofs can take hundreds of millions of tokens to produce”. I token sono i pezzetti di testo che un modello legge e scrive, e sono l’unità con cui si paga l’uso dell’AI. Quindi le prove possono costare centinaia di milioni di token. Quanto è costato il progetto in totale, Anthropic non lo dichiara. Non lo sappiamo e non ha senso fare stime a occhio (Anthropic).

Anche sul modello usato la fonte è scarna: per il progetto principale scrive soltanto “Claude”.

Fin qui, il numero impressiona meno. Ma è anche più onesto, e ti dà un metodo: quando senti un numero, chiediti di che cosa è il numero.

Cosa dimostra la prova: una frase sola

Righello disegnato a mano su fondo beige: un tratto iniziale evidenziato in grigio chiaro con un segno di spunta, il resto tratteggiato.

Eccola. Per ogni input sotto i 64 MB, il programma non va in crash (Anthropic).

Tutto qui. Non “il programma fa la cosa giusta”. Non “il programma è sicuro”. Non va in crash, qualunque cosa tu gli dia in pasto entro quella soglia.

C’è un secondo dettaglio che cambia la lettura. Chi ha scritto la specifica, cioè la regola che la prova deve rispettare? Non un essere umano da zero. La specifica viene dai test casuali che esistevano già per quelle librerie (Anthropic). Il repository pubblico delle prove la descrive come un “accordo”: la versione normale del programma e quella con gli strumenti di controllo si comportano allo stesso modo, senza errori, su ogni input entro i limiti (theorem-labs/oss-verify-proofs, GitHub).

Conseguenza: la prova è forte quanto il test da cui nasce. Se il test non guardava una certa cosa, la prova non la copre.

E ci sono le ipotesi. I programmi verificati sono binari per il processore RISC-V, statici, a un solo filo di esecuzione, collegati alla libreria di base musl, eseguiti su Linux con memoria fissa. La fonte ammette che quasi tutti usano invece x86 o ARM con la libreria glibc dinamica (Anthropic). Detto da un fotografo: hai dimostrato che l’obiettivo è nitido, ma su un banco ottico in laboratorio, non sulla macchina che porti in giro.

Poi c’è la parte su cui ci si deve fidare e basta: per verificare zlib su x86 si usa una descrizione del processore generata da Claude stessa e “heavily tested” (Anthropic). Testata a fondo, quindi, non dimostrata.

E la frase che vale tutto il pezzo la scrive Anthropic stessa, nella sezione dei limiti:

“Formally verified” does not mean “bug-free.”

Più avanti, un’altra, ancora più netta: un controllore di prove non può dirti se la specifica corrisponde alla realtà (Anthropic). Il controllore verifica che la dimostrazione sia corretta. Se la domanda che hai dimostrato è quella sbagliata, il controllore ti dirà “ok” lo stesso.

I bug trovati: la parte concreta

Qui il lavoro diventa interessante, e per una ragione che non è quella dei titoli. Mentre provavano a scrivere le prove, Claude e il team hanno trovato “hundreds of bugs”, centinaia di bug (Anthropic).

Alcuni esempi, che ti aiutano a capire perché un test normale non li vede:

  • In un programma che decomprime file, un contatore poteva scendere sotto zero e provocare una scrittura fuori dal posto previsto. Succedeva solo con un input di circa 20 MB.
  • In un programma che legge immagini, c’era una lettura fuori dai limiti. Per farla scattare servivano un input da 64 MB e oltre 2 GB di memoria.
  • È stata ritrovata la vulnerabilità nota CVE-2026-56132 in libexpat.
  • Un bug “logico”: una funzione che dovrebbe limitare quali file un’applicazione può caricare non veniva sempre applicata.
  • Un altro bug logico, rimasto nascosto per più di dieci anni in un software che la fonte non nomina.

(Tutti dalla stessa fonte: Anthropic, 22 ottobre 2026.)

Capisci perché i test normali li mancano: nessuno prova un file da 20 MB solo per vedere se un contatore va sotto zero. Una dimostrazione, invece, deve coprire tutti gli input, quindi è costretta ad arrivarci.

Su un lettore di PDF molto diffuso, sempre secondo la fonte, sono emersi “as many security bugs in one week as are typically reported in a year”. Cioè in una settimana tanti bug di sicurezza quanti ne vengono segnalati di solito in un anno (Anthropic).

Questo risponde anche a chi dice “una prova che garantisce solo il non-crash non vale niente”. Non è niente. I bug che ho citato sono letture e scritture fuori limite, e la fonte stessa parla di bug di sicurezza. Ma, come vedi, vale per quello che ha coperto e non oltre.

Resta da chiarire che cosa vuol dire “corretti”. La fonte scrive che hanno lasciato a Claude il compito di correggere i bug trovati. È una patch proposta da Claude, non una correzione già accettata dai gestori delle librerie. L’unico caso in cui la fonte dice qualcosa sul passaggio ai gestori è zlib: bug minori, non sfruttabili, “in the process of being filed upstream”, cioè in corso di segnalazione (Anthropic). Per tutti gli altri non sappiamo. E alcune prove non sono state pubblicate proprio per non rivelare bug ancora aperti.

Può barare? Il punto che riguarda anche te

Qui c’è il passaggio che mi è piaciuto di più, perché Anthropic ammette il rischio da sola.

Se chiedi a un’AI “fammi dimostrare che questo programma non crasha”, la scorciatoia è dietro l’angolo: riscrivere il programma in uno che non fa niente, e quindi non crasha mai. La fonte lo scrive così: Claude potrebbe rendere dimostrabile qualunque teorema “by rewriting the program into one that trivially never crashes” (Anthropic).

È la versione tecnica di uno studente che, per non sbagliare il compito, consegna il foglio bianco. Il foglio bianco non ha errori.

Le contromisure dichiarate: le patch vengono penalizzate, c’è un premio extra per chi dimostra quali input una patch cambia e quanto pochi sono, e le patch vengono registrate e controllate a posteriori (Anthropic). Nota che la misura è sugli input toccati, non un giudizio generico sulla bontà della patch.

Il principio dietro, però, vale più della contromisura: chi controlla non deve essere chi lavora. Lo stesso principio compare nella guida ufficiale di Claude Code, dove si consiglia di far rivedere il lavoro a un secondo agente in un contesto pulito, “so the agent doing the work isn’t the one grading it” (Claude Code docs, Best practices). Hai già visto cosa succede quando un agente lavora senza qualcuno che lo controlla: ne ho parlato in Claude ha cancellato l’HD di 50 persone. La colpa è tua e in Duecento email cancellate mentre lei scriveva STOP.

Perché finora era rara e cara

Se la verifica formale esiste da anni, perché non la usano tutti? Perché costava un’enormità, fatta a mano da specialisti.

Il caso storico è seL4, un nucleo di sistema operativo: circa 8.700 righe di C e 600 di assembly, verificate con controllo automatico. Il paper del 2010 specifica che la dimostrazione assume corretti il compilatore, il codice assembly, l’hardware e il codice di avvio (Klein et al., CACM 53(6), 2010). Anche lì, cioè, qualcosa va creduto sulla fiducia.

Sui costi ho una fonte datata, quindi te lo dico con la data: nel 2016 Gernot Heiser, uno degli autori di seL4 (quindi di parte), stimava meno di 400 dollari per riga di codice, con un fattore 2-3 rispetto allo stesso tipo di software non verificato, e oltre 20 righe di prova per ogni riga di C, scritte a mano (Heiser, microkerneldude.org, 16 giugno 2016).

Anche AWS usa ragionamento automatico “in key service areas such as storage, networking, virtualization, identity, and cryptography” (AWS, Provable security), e ha usato il linguaggio TLA+ per specificare una decina di sistemi grandi e complessi (Newcombe et al., CACM, aprile 2015).

Ora Theorem, nel suo blog del 29 settembre 2026 (aggiornato il 19 ottobre), fa delle proiezioni. Le riporto come stime di Theorem, perché è un’azienda che ha tutto l’interesse a presentarle bene: verificare il 95% del codice macchina di nixpkgs (una grande raccolta di pacchetti software) entro fine 2027, con un costo stimato di circa 134 milioni di dollari. Per OpenSSL, circa 220.000 dollari. La velocità di produzione delle prove sarebbe passata da circa 0,12 KB di codice all’ora a 0,6-0,9 KB all’ora, misurata su 36 piccoli programmi C (Theorem, Bootstrapping the Verified Software Stack).

Una precisazione: non mettere questi numeri in fila a quelli di seL4 per ricavare “quanto costa meno”. Non sono confrontabili. seL4 è un costo a riga di C per una correttezza funzionale completa, fatta a mano. Quello di Theorem è una proiezione per kilobyte di codice macchina, su una proprietà molto più ristretta. Li metto accanto come contesto: ti dicono in che direzione si muove il discorso (le prove le scrive la macchina, non uno specialista), non di quanto.

Cosa arriva davvero a chi non programma (spoiler: poco)

Arriviamo alla domanda che ti interessa: posso usarla?

La risposta onesta è no, non oggi, non sui tuoi script.

La fonte di Anthropic dice che Theorem pubblica “a Claude skill to help developers get started with verifying their own code”. Letta così, sembra uno strumento per verificare il proprio codice. Sono andato a leggere la skill sul repository: serve a iscrivere un progetto open source a OSS Verify, insieme al suo gestore, e richiede prerequisiti tecnici come clang, llvm e qemu-riscv64 (theorem-labs/oss-verify, skill add-project). Non è un bottone da premere sul tuo script Python.

OSS Verify, il servizio, è gratuito per i progetti open source idonei, e l’adesione passa da una pull request (una proposta di modifica) fatta dai gestori principali del progetto. Le prove possono richiedere “multiple days”, più giorni, e la priorità è per programmi in C con binari piccoli (Theorem, OSS Verify).

Il repository pubblico delle prove contiene oggi 60 punti di ingresso in 25 librerie, un sottoinsieme dei 239 dell’annuncio (theorem-labs/oss-verify-proofs). Le prove che potrebbero rivelare un bug non ancora corretto non sono state pubblicate.

Cosa non sappiamo, per essere chiari: i prezzi per chi non è un progetto idoneo, se l’approccio funzioni oltre le librerie testate, che modello abbia fatto il lavoro nel dettaglio.

Un esempio che va oltre le librerie c’è: un interprete di un sottoinsieme di Python, scritto in Rust e verificato con uno strumento chiamato Verus, che nei test su oltre 1,7 milioni di programmi Python casuali si comporta come CPython nel 99,95% dei casi (Anthropic). Occhio però: è un test a campione molto grande, non una prova totale. Il 99,95% non è il 100%.

Cosa portare a casa senza verifica formale

Griglia di piccole cornici fotografiche disegnate a mano su fondo beige: in primo piano una fila ordinata di venti campioni spuntati, e una scheda isolata con l'icona di un calendario vuoto.

Se per te “dimostrazione formale” resta lontana, vale la lezione che ci sta sotto. La logica scende fino a te, anche se lo strumento no.

Immagina di chiedere a un’AI uno script che rinomina 3.000 foto e le sposta in cartelle per data. Lo lanci. Sembra funzionare. Tre mesi dopo scopri che le foto senza data di scatto sono finite tutte nella stessa cartella, senza avviso. È il mondo in cui vive chi si fa scrivere script senza altro controllo.

Le linee guida ufficiali di Claude Code lo dicono con una frase che vale la pena di tenere a mente: senza un controllo eseguibile “looks done” è l’unico segnale disponibile, e sei tu il ciclo di verifica (Claude Code docs, Best practices).

Quindi, tre abitudini.

1. Dai all’AI un controllo che può eseguire. La guida lo scrive così: “Give Claude a check it can run: tests, a build, a screenshot to compare.” Per lo script delle foto, un controllo può essere: una cartella di 20 foto di prova, compresa qualcuna senza data, e un elenco di come devono finire. Lo script gira sulle 20 prima di toccare le 3.000.

2. Chiedi evidenze, non dichiarazioni di successo. Sempre dalla guida: l’AI deve mostrare “the test output, the command it ran and what it returned, or a screenshot of the result” (Claude Code docs). “Tutto a posto” non è un’evidenza. L’output del controllo, sì.

3. Fai guardare il lavoro a un secondo sguardo. Un secondo agente, in una conversazione pulita, che rilegge ciò che ha fatto il primo. Con una cautela che segnala la stessa guida: se rincorri ogni singolo rilievo finisci per sovra-ingegnerizzare. Prendi quelli che contano.

E poi c’è la frase conclusiva della guida, sul “buco della fiducia”: “If you can’t verify it, don’t ship it.” Se non puoi verificarlo, non consegnarlo (Claude Code docs).

Un’aggiunta che è mia, non della guida, e la dichiaro come tale: chiedi all’AI di scriverti che cosa il controllo copre e che cosa no. Deriva dalla distinzione che Anthropic fa tra specifica e realtà. Se il tuo controllo prova solo con file che hanno la data, dillo, e sai già dove il tuo script è scoperto.

Ora la precisazione che ti devo, perché è il punto in cui è facile scivolare. Un test eseguibile e una prova formale non sono la stessa cosa, e non sono nemmeno gradi vicini della stessa scala. Un test copre i casi che hai provato. Una prova copre tutti gli input entro la specifica. Il principio (un controllore separato da chi lavora, l’evidenza al posto della dichiarazione) si trasferisce dal mondo delle prove al tuo script. La garanzia no. Avere tre test che passano non è “la mia piccola verifica formale”: è la prova che quei tre casi vanno, e solo quelli.

“Ma è marketing”

Obiezione sensata, e in parte vera. Le due fonti principali sono di chi ha un interesse: Anthropic vende Claude, Theorem vende verifica, e la roadmap di Theorem è una proiezione aziendale. Per questo l’ho tenuta come stima e non come fatto.

Due cose però vanno a favore della fonte: dichiara in chiaro i limiti (le ipotesi sui binari, “verified non vuol dire senza bug”, il rischio di barare, le prove non pubblicate) e il repository delle prove è pubblico, quindi chi sa leggerlo può controllare. Resta un limite mio: nelle ricerche per questo pezzo non ho trovato voci critiche indipendenti di esperti. Se ne leggi, mandamele.

Cosa fare adesso

Tre cose, in ordine di fatica.

  1. Alla prossima notizia con “l’AI dimostra” nel titolo, fai tre domande: cosa è stato dimostrato, su quali input, rispetto a quale specifica. Se non trovi le risposte nella fonte primaria, il titolo sta vendendo più di quello che c’è.
  2. Per il prossimo script, prima di lanciarlo sui dati veri, fallo girare su pochi casi di prova, compresi quelli scomodi, con l’output davanti a te.
  3. Fatti dire cosa non è coperto, e annotalo accanto allo script: fra sei mesi te ne sarai dimenticato.

Se vuoi capire perché oggi tutto questo conta, tieni d’occhio il filone sugli agenti che lavorano da soli e sui controlli che mancano, che ho raccontato in Stiamo installando un nuovo sistema operativo. E non lo sappiamo.

La verifica formale, forse, un giorno diventerà qualcosa che si compra. Intanto la domanda che ha reso possibile tutto questo lavoro è gratis, e la puoi fare già oggi: cosa mi garantisce che funziona?

Se hai uno script che usi ogni settimana e non sai davvero che cosa fa nei casi strani, scrivimelo in risposta a questa mail. Ci costruiamo insieme un controllo da dargli in pasto.

Luca

Articoli correlati

Fonti

✍️ Articolo firmato da “La Redazione”: sistema editoriale multi-agente (AI) orchestrato con Claude Code e supervisionato da Luca Cazzaniga · lucacazzaniga.it

Leggi anche

AI