Buterin afferma che la verifica formale dell'IA aumenta la sicurezza delle criptovalute

Buterin pubblica un nuovo post su IA e sicurezza del codice

Il cofondatore di Ethereum Vitalik Buterin ha pubblicato un post sul blog il 18 maggio 2026 su vitalik.eth.limo. In esso, sostiene che la verifica formale assistita dall'IA diventerà uno degli strumenti più importanti della cybersicurezza. La verifica formale è un metodo che utilizza prove matematiche per confermare che il software si comporta esattamente come previsto. Buterin afferma che combinare l'IA con la verifica formale aiuterà gli sviluppatori a trovare vulnerabilità prima che lo facciano gli attaccanti.

Claude Mythos citato come esempio del potere dell'IA

Buterin nomina Claude Mythos, un modello di IA sviluppato da Anthropic, come esempio di sistemi di IA sempre più potenti. Sostiene che tali sistemi possono accelerare la scoperta e lo sfruttamento delle vulnerabilità. Claude Mythos è un modello reale. Anthropic ha confermato la sua esistenza dopo una fuga di dati accidentale nel marzo 2026. Una preview del modello è stata rilasciata a partner selezionati nell'aprile 2026.

Buterin elenca i limiti della verifica formale

Buterin sottolinea che la verifica formale non elimina tutti i rischi. I sistemi di prova possono trascurare assunzioni critiche o non coprire vulnerabilità hardware e superfici di attacco adiacenti. Avverte anche che l'IA abbassa la barriera per generare grandi volumi di software. Ciò aumenta il rischio che codice insicuro o poco compreso entri nei sistemi di produzione. Nonostante questi limiti, Buterin sostiene che l'approccio riduce il rischio catastrofico rispetto allo sviluppo software tradizionale.

Il progetto Arklib punta a un'implementazione STARK verificata

Buterin evidenzia Arklib come un esempio concreto di metodi formali applicati a Ethereum. Arklib è un progetto open-source che mira a costruire un'implementazione completamente verificata formalmente di un sistema di prove STARK. Un STARK è un tipo di prova crittografica utilizzata nell'infrastruttura di scalabilità di Ethereum. La Ethereum Foundation ha finanziato Nethermind per estendere Arklib con la formalizzazione del protocollo FRI nell'assistente alla prova Lean. Buterin fa anche riferimento a implementazioni verificate formalmente della Ethereum Virtual Machine scritte direttamente in assembly RISC-V.