Vitalik Buterin, co-fondatorul Ethereum, a răspuns preocupărilor tot mai mari conform cărora vânătoarea de bug-uri bazată pe IA va copleși dezvoltatorii și va crea oportunități de exploatare non-stop pe blockchain-uri. Potrivit acestuia, în viitorul apropiat, utilizarea acestei tehnologii ar putea face de fapt sistemele cripto mai sigure. El spune că verificarea formală asistată de IA ar putea deveni una dintre cele mai puternice apărări împotriva eșecurilor de securitate în cripto și infrastructura internetului.
IA Ar Putea Consolida Securitatea În Loc Să O Distrugă
Verificarea formală este practica de a scrie dovezi matematice despre software pe care un computer le poate verifica automat în loc să le revizuiască oamenii. Acest concept este disponibil de zeci de ani; cu toate acestea, nu a prins niciodată, deoarece generarea manuală a unor astfel de dovezi era destul de obositoare pentru dezvoltatorii de software, așa că mulți dintre ei nu s-au deranjat niciodată.
Acum, Buterin spune că IA a schimbat această ecuație și, în loc ca dezvoltatorii să scrie singuri dovezile, ei pot cere unei IA să scrie atât codul, cât și dovezile însoțitoare. Apoi, ei verifică pur și simplu dacă declarația finală dovedită este de fapt lucrul pe care au vrut să-l dovedească.
Dezvoltatorul a descris un scenariu în care modelele IA devin suficient de puternice pentru a automatiza găsirea de bug-uri în codul existent și apoi a întrebat ce ar însemna asta pentru sistemele în care o singură eroare poate costa utilizatorii totul. Răspunsul său a fost că verificarea formală, făcută end-to-end, vă permite să demonstrați matematic că o bucată de cod se comportă exact așa cum a fost intenționat, astfel încât o IA suficient de puternică care caută erori s-ar uita la cod care a fost deja dovedit că nu le are.
El a menționat, de asemenea, proiecte specifice de infrastructură Ethereum în care această abordare este deja încercată. Unul dintre ele este Arklib, care lucrează la o implementare STARK complet verificată formal. Un altul este evm-asm, care construiește un EVM scris în assembly RISC-V de nivel scăzut și verifică corectitudinea acestuia în raport cu o implementare de referință lizibilă de oameni.
Cu privire la întrebarea despre care modele IA sunt de fapt utile pentru acest lucru, Buterin a spus că a constatat că Claude și Deepseek 4 Pro sunt ambele suficiente pentru a scrie dovezi Lean. El a semnalat, de asemenea, Leanstral, un model mai mic cu greutăți deschise, fin reglat special pentru Lean, ca fiind capabil să ruleze local și să depășească modelele de uz general mult mai mari pe reperele de verificare formală.
Dar Există Limite
În ciuda entuziasmului său pentru verificarea formală, Buterin a dedicat, de asemenea, o parte substanțială din eseul său explicării modurilor în care a eșuat în practică. Aceasta include bug-uri în compilatoarele verificate; biblioteci unde doar o parte din cod a fost dovedită, iar părțile nedovedite s-au dovedit a fi problema; și specificații care au fost dovedite tehnic, dar pur și simplu nu au surprins ceea ce dezvoltatorul a vrut de fapt să garanteze.
Cu toate acestea, încadrarea sa mai largă este că verificarea formală nu este un înlocuitor pentru toate practicile de securitate, ci un instrument puternic într-o tendință de lungă durată către mai puține bug-uri pe linie de cod.
Contextul este relevant aici, având în vedere că în ziua în care a apărut postarea lui Buterin, sectorul cripto era zdruncinat de o a treia exploatare majoră în doar patru zile, după ce un hacker a fugit cu criptomonede în valoare de peste 76 de milioane de dolari de pe puntea cross-chain a Echo Protocol. Cu câteva zile mai devreme, au apărut rapoarte despre un hack asupra THORChain, care a costat platforma peste 10 milioane de dolari. Un alt atac s-a întâmplat după acesta, vizând Verus-Ethereum Bridge, prin care un hacker a profitat de lipsa unei verificări de validare pentru a fura 11,58 milioane de dolari. Acesta este genul de defect specific, localizat, pe care o verificare formală a dovezilor l-ar fi putut detecta.