Anthropic ha annunciato che il suo modello Claude è in grado di generare automaticamente prove di verifica formale per codice già esistente. In un test condotto su 123 librerie del progetto OSS‑Fuzz di Google, Claude ha generato circa 180 milioni di righe di prove nell’arco di poche settimane. Le prove sono state verificate con il verificatore Rocq e, secondo Anthropic, il processo ha richiesto pochissimo intervento umano.
Cosa ha fatto davvero il sistema
Claude non ha scritto nuovi programmi. Ha invece trasformato casi di test che provocavano crash in enunciati matematici, analizzato il codice macchina compilato e prodotto prove formali che dimostrano la conformità del codice a quegli enunciati. Quando il modello ha incontrato un bug, gli è stato consentito di correggere il codice. In una settimana di verifiche su un diffuso lettore di PDF, Claude ha scoperto tanti bug di sicurezza quanti se ne segnalano di solito in un anno intero. In un’altra libreria ha trovato un errore logico rimasto nascosto per più di dieci anni.
Limiti e costi
Anthropic avverte che le prove valgono solo per programmi a thread singolo eseguiti su una specifica architettura di processore e con input inferiori a 64 MB. Il calcolo richiesto è oneroso: per singole prove si arriva a centinaia di milioni di token, anche se l’azienda non ha comunicato la spesa complessiva. Un test più piccolo ha mostrato che il modello più recente Opus 5.5 può completare metà delle prove usando circa il 40 % di token in meno rispetto al predecessore.
Perché conta
Se l’IA riuscisse a verificare automaticamente il codice, gli sviluppatori potrebbero dedicare meno tempo alla ricerca di bug e alla revisione delle correzioni, soprattutto nei software critici per la sicurezza. L’approccio attuale, però, funziona solo entro limiti rigorosi di hardware e dimensione degli input: per la maggior parte delle applicazioni di uso quotidiano restano necessari i test tradizionali.
