Anthropic afferma che Claude ha scritto prove formali secondo cui 123 librerie open source non possono andare in crash

In collaborazione con Theorem, Anthropic afferma di aver usato Claude per dimostrare proprietà di sicurezza a livello di assembly (RISC-V) in oltre 100 librerie open source usate nel mondo reale. L’azienda definisce il lavoro il primo impiego su larga scala dell’AI per verificare formalmente software di produzione a quel livello.

Secondo Anthropic:

• Cosa è stato dimostrato: per 239 punti di ingresso ai test di fuzzing distribuiti in 123 librerie OSS-Fuzz, i programmi terminano sempre normalmente, senza errori di sicurezza della memoria né asserzioni non soddisfatte, per ogni input inferiore a 64 MB. Questo vale a determinate condizioni: un binario statico a singolo thread, con un budget di memoria fisso, su una CPU RISC-V che esegue Linux. Le prove ammontano a circa 180 milioni di righe di Rocq, verificate dal proof checker di Rocq.
• Come: il test di fuzzing esistente di ogni libreria è stato trasformato in una specifica («questo test non va mai in crash») e Claude ha scritto la prova, correggendo nel frattempo i bug individuati. Anthropic afferma che questo ha permesso di trovare centinaia di bug, compresi quelli difficili da raggiungere con un fuzzer, come una scrittura fuori dai limiti che richiede un raro input da 20 MB, e la riscoperta di CVE-2026-56132 in libexpat.
• Altri esperimenti: Claude ha dimostrato che l’implementazione di zlib nel kernel Linux corrisponde a una specifica di RFC 1950 a livello di binario x86 e ha creato un interprete Python in Rust il cui comportamento coincideva con quello di CPython nel 99,95% di 1,7 milioni di programmi casuali. Anthropic afferma inoltre che i tentativi di verifica formale su un lettore PDF molto diffuso hanno portato alla luce in una settimana tanti bug di sicurezza quanti ne vengono segnalati tipicamente in un anno.
• Costo: le prove possono richiedere centinaia di milioni di token. Su 36 piccoli compiti di verifica, Anthropic afferma che Opus 5.5 ne dimostra la metà usando circa il 40% di token in meno rispetto a Opus 5, e che gli agenti che condividevano le prove hanno richiesto il 17% di token in meno.

Anthropic pubblica una parte delle prove e la semantica di RISC-V e Linux. Theorem si offre di eseguire la stessa pipeline per altri progetti open source e pubblica una skill di Claude per verificare il proprio codice. Anthropic precisa che questo non dimostra che le librerie siano prive di bug: quelli ancora presenti si troverebbero nei componenti considerati attendibili o al di fuori dell’ambito delle prove.