Anthropic afferma che Claude ha dimostrato che 123 librerie open-source non possono andare in crash

Anthropic afferma che Claude ha dimostrato matematicamente che il codice sottoposto a fuzz testing in 123 librerie open-source non può bloccarsi con input inferiori a 64 MB, e ha inoltre individuato bug che anni di test erano sfuggiti.

Il lavoro, pubblicato da Anthropic il 22 ottobre In collaborazione con la startup di verifica formale Theorem, il progetto copre 239 punti di ingresso del progetto OSS-Fuzz di Google. Anthropic lo definisce il primo sforzo su larga scala per utilizzare l'intelligenza artificiale nella verifica formale del software di produzione a livello di codice assembly.

Dai test alle dimostrazioni

Il fuzzing consiste nell'inviare un numero enorme di input casuali a un programma per vedere cosa si blocca, ma non può mai provare ogni singolo input. Anthropic ha trasformato ogni test di fuzzing esistente in una regola formale, "questo test non si blocca mai", e ha chiesto a Claude di dimostrare che ciò vale per ogni input inferiore a 64 MB.

Le dimostrazioni funzionano sul codice macchina RISC-V compilato anziché sul codice sorgente. Nel giro di poche settimane, Claude ha scritto circa 180 milioni di righe di dimostrazioni nell'assistente di dimostrazione Rocq, circa 600.000 righe per un programma tipico. Nessun essere umano deve leggerle; il verificatore Rocq le conferma automaticamente una per una.

Test dei bug mancati

Ogni volta che una dimostrazione falliva, Claude trovava un bug, lo correggeva e riprovava. Anthropic afferma che questo lavoro ha portato alla luce centinaia di bug, tra cui una scrittura fuori dai limiti in un decompressore che si verificava solo con input di circa 20 MB e un layout raro, e la riscoperta di un difetto noto nel parser XML di libexpat.

In test separati, Claude ha dimostrato che il codice zlib del kernel Linux corrisponde alle specifiche del formato e, nel tentativo di verificare un lettore PDF ampiamente utilizzato, ha trovato in una settimana tanti bug di sicurezza quanti ne vengono in genere segnalati in un anno. I dettagli sono nel appendice tecnica.

Ciò che non dimostra

Anthropic specifica esplicitamente che "formalmente verificato" non significa privo di bug. Le dimostrazioni presuppongono binari RISC-V a singolo thread e collegati staticamente su Linux, mentre la maggior parte delle implementazioni reali viene eseguita su architetture x86 o ARM. I controlli di memoria utilizzati non rilevano tutti i bug di sicurezza della memoria e non tutti i punti di ingresso in ciascuna libreria sono stati coperti.

L'altro problema è il costo: le prove possono richiedere centinaia di milioni di token. Anthropic afferma che Claude Opus 5.5 ha risolto metà di un benchmark di 36 attività con circa 40% di token in meno rispetto a Opus 5, e gli agenti che hanno condiviso le prove hanno utilizzato 17% di token in meno.

Perché è importante

L'IA sta diventando molto brava a trovare bug, poiché Difetti di PHP2Shell mostrato questa settimana. Le dimostrazioni sono un modo per dimostrare che intere classi di bug semplicemente non esistono. Theorem ha rilasciato un Claude abilità per i manutentori open-source che vogliono iscrivere i loro progetti, e stime che 95% del codice macchina nell'ecosistema software Nix potrebbero essere verificati entro la fine del 2027 per circa 134 milioni di dollari.