Claude dimostra che 123 librerie software non vanno in crash: ecco i limiti

Circa 180 milioni di righe per dimostrare che alcuni programmi non vanno in crash. È la quantità di codice di prova che, secondo Anthropic, Claude ha prodotto in poche settimane lavorando su 123 librerie open source. Nel tentativo di costruire quelle dimostrazioni, l’AI ha anche individuato centinaia di bug, alcuni rimasti nascosti per anni. Sono risultati notevoli, ma non significano che le 123 librerie siano diventate immuni da ogni errore.

La ricerca, pubblicata il 22 ottobre 2026 e condotta con la società Theorem, affronta un problema che cresce insieme agli strumenti di programmazione AI: scrivere codice più in fretta serve a poco se non riusciamo a controllarlo con altrettanta cura. Qui Claude non si è limitato a cercare difetti. Ha scritto prove formali, cioè dimostrazioni espresse in un linguaggio matematico che un programma separato può controllare.

La distinzione riguarda anche noi in Italia: le librerie open source sono componenti riutilizzati in prodotti e servizi ben oltre il Paese in cui vengono sviluppati. Capire che cosa sia stato davvero dimostrato conta più dell’etichetta «software sicuro».

Un test tradizionale prova il programma con alcuni input e osserva che cosa succede. Il fuzzing è una versione intensiva di questo metodo: genera moltissimi dati insoliti o modificati per provocare errori. È come collaudare una serratura con un’enorme quantità di chiavi: trovare quella che la rompe è prezioso, ma non trovarla non prova che nessuna chiave possa farlo. Il progetto OSS-Fuzz di Google applica continuamente questa tecnica al software open source.

Anthropic e Theorem sono partite proprio dai punti d’ingresso usati dai test di OSS-Fuzz: funzioni predisposte dagli sviluppatori per ricevere dati e segnalare un problema tramite un crash. Hanno trasformato la richiesta «questo test non deve andare in crash» in una specifica, ovvero una regola precisa da dimostrare. Claude ha quindi cercato una prova valida per tutti gli input coperti dalla specifica, anziché limitarsi a eseguirne un gran numero.

Il gruppo dichiara di aver completato prove per 239 punti d’ingresso in 123 librerie. Le dimostrazioni riguardano i programmi già compilati in istruzioni RISC-V, un’architettura di processore: in altre parole, ragionano su una versione eseguibile del software, non soltanto sulle righe scritte dallo sviluppatore. Una prova tipica conta circa 600.000 righe nel linguaggio Rocq.

Claude produce la dimostrazione, ma non è Claude a darle il voto finale. La controlla Rocq, un assistente alla dimostrazione: un software che verifica se ogni passaggio rispetta le regole logiche e conduce alla conclusione dichiarata. Il paragone utile è quello di un calcolo lunghissimo svolto da un collaboratore e ricontrollato da uno strumento indipendente: non occorre fidarsi della sicurezza con cui il collaboratore presenta il risultato.

Per costruire il problema da risolvere servono però anche un modello matematico delle istruzioni RISC-V e uno del comportamento del sistema operativo Linux. La prova è valida rispetto a quei modelli e all’enunciato scelto. Anthropic indica proprio nei modelli, nell’enunciato e nel controllore Rocq gli elementi da verificare con particolare attenzione: una dimostrazione impeccabile della regola sbagliata non rende sicuro un prodotto reale.

C’è anche un elemento verificabile da altri ricercatori. Nel repository pubblico di Theorem sono disponibili prove per 60 punti d’ingresso in 25 librerie: un sottoinsieme del lavoro complessivo annunciato da Anthropic, non tutti i 239 casi. Il progetto precisa inoltre che quelle prove riguardano specifici file eseguibili e non certificano l’intera libreria.

Il risultato più concreto non è solo la quantità di prove prodotte. Quando Claude non riusciva a completarne una, il motivo poteva essere un difetto reale: il gruppo gli ha consentito di correggere il codice e poi di tentare una nuova dimostrazione sulla versione modificata. Secondo Anthropic, questo processo ha portato alla scoperta di centinaia di bug.

Tra gli esempi descritti da Anthropic c’è un errore in un decompressore che richiedeva un input di circa 20 megabyte con una disposizione molto rara dei dati. Il gruppo riferisce anche di una lettura oltre i limiti della memoria in un decodificatore di immagini, legata a input e consumi di memoria insolitamente grandi. Sono condizioni che una ricerca basata su tentativi, pur intensa, può incontrare con difficoltà.

Non tutti i difetti, però, fanno chiudere un programma. I ricercatori raccontano di aver notato anche un problema logico in una funzione pensata per limitare i file caricabili da un’applicazione. È un promemoria importante: dimostrare l’assenza di crash e verificare che il software faccia sempre la cosa giusta sono obiettivi diversi.

Le prove principali coprono gli input inferiori a 64 megabyte per i punti di test verificati, sotto ipotesi precise: programmi compilati per RISC-V, a thread singolo, con risorse di memoria definite e un comportamento di Linux rappresentato dal modello. Molti impieghi reali delle stesse librerie usano invece altri processori, altre modalità di compilazione e applicazioni che chiamano il codice in modi non coperti dai test. Anthropic riconosce esplicitamente questa distanza tra esperimento e uso quotidiano.

Il repository di Theorem aggiunge una precisazione utile: le prove pubblicate non escludono che un’esecuzione continui all’infinito. Non dimostrano neppure che ogni risultato prodotto dalla libreria sia corretto o che ogni sua funzione sia coperta. Escludono gli errori specificati per il codice raggiungibile da quei punti d’ingresso, nelle condizioni modellate.

C’è infine la questione delle risorse. Anthropic osserva che produrre prove può richiedere enormi quantità di token, le unità di testo elaborate dai modelli AI, e non comunica un costo totale per questo esperimento. Su 36 compiti di verifica più piccoli, il gruppo riferisce che Claude Opus 5.5 completa metà dei compiti usando circa il 40% di token in meno rispetto a Opus 5: un progresso misurato in quel test, non la prova che verificare qualsiasi programma sia già economico.

Anthropic punta a rendere la verifica formale abituale quanto i test. Per arrivarci, non basterà chiedere all’AI di scrivere più dimostrazioni: serviranno modelli affidabili dei sistemi reali e prove che possano essere riutilizzate quando più programmi dipendono dalla stessa libreria. Nel suo piano di ricerca, Theorem propone di partire proprio dalle dipendenze condivise, come OpenSSL, usate da molti altri pacchetti. È una prospettiva, non un risultato già raggiunto su tutti quei programmi.

Per chi sviluppa servizi in Europa o in Italia, la conseguenza potenziale è concreta: una prova attendibile su un componente condiviso potrebbe essere utile a molti progetti, anche se nati altrove. Ma ogni riuso dovrebbe conservare ben visibili le condizioni della garanzia. Un certificato che nessuno sa interpretare rischia di rassicurare più di quanto protegga.

Claude ha mostrato che l’AI può contribuire non solo a scrivere software, ma anche a sottoporlo a domande molto più rigorose dei normali test. La domanda decisiva, d’ora in poi, non sarà soltanto «c’è una prova?». Sarà: che cosa prova, esattamente?