• Inteligența artificială începe să schimbe securitatea din crypto, ajutând dezvoltatorii să găsească mai repede buguri în smart contracts
• Formal verification folosește matematică pentru a demonstra că un contract inteligent respectă reguli critice, nu doar că trece câteva teste
• Vitalik Buterin spune că AI-ul și verificarea formală pot deveni esențiale pentru securitatea blockchain, dar avertizează că metoda nu repară ipotezele greșite
• Chainalysis estimează că peste 3,4 miliarde de dolari în criptomonede au fost furați în 2025, inclusiv 1,5 miliarde de dolari în atacul asupra Bybit
• Riscul major este că aceeași AI care ajută auditorii poate ajuta și atacatorii să descopere vulnerabilități mai repede

În lumea obișnuită a software-ului, un bug poate însemna o aplicație care se blochează, un buton care nu merge sau un update neplăcut. În crypto, un bug poate însemna că banii dispar înainte să apuci să deschizi dashboard-ul. Un smart contract nu sună la suport, nu așteaptă aprobare de la bancă și nu are buton de „undo”. Execută ce scrie în cod. Iar dacă în cod există o portiță, cineva o poate transforma în jaf.

De aici vine interesul nou pentru formal verification, o metodă veche din informatică, dar greu de folosit la scară largă. Ideea este simplă în teorie și dificilă în practică: în loc să testezi codul doar pe câteva scenarii, încerci să demonstrezi matematic faptul că anumite lucruri rele nu se pot întâmpla.

Tema a revenit în prim-plan după ce Vitalik Buterin, cofondatorul Ethereum, a scris pe 18 mai 2026 că inteligența artificială ar putea face sistemele crypto și infrastructura digitală critică mai sigure, dacă este combinată cu software verificat matematic. Potrivit CoinDesk, Buterin vede AI-assisted formal verification ca pe una dintre cele mai importante direcții pentru securitate, într-un moment în care modelele AI devin tot mai bune și la descoperirea vulnerabilităților.

Contextul financiar explică de ce industria nu mai poate trata securitatea ca pe o anexă tehnică. Chainalysis estimează că peste 3,4 miliarde de dolari în criptomonede au fost furați în 2025, până la începutul lunii decembrie, iar compromiterea Bybit din februarie 2025 a reprezentat singură 1,5 miliarde de dolari din total.

Altfel spus, discuția nu este despre un moft academic. Este despre cum protejezi contracte care pot ține, muta sau bloca sume uriașe fără intervenție umană directă.

Formal verification este detectorul de minciuni al codului

Formal verification este un fel de examen de matematică pentru cod. Dezvoltatorii stabilesc reguli clare: fondurile nu pot dispărea, un utilizator nu poate retrage mai mult decât are, tokenurile nu pot fi create din nimic, iar contractul nu poate bloca banii pentru totdeauna. Apoi, instrumentele de verificare încearcă să demonstreze că aceste reguli rămân adevărate în toate situațiile relevante.

Documentația Ethereum descrie formal verification ca o tehnică recomandată pentru îmbunătățirea securității contractelor inteligente, tocmai pentru că smart contracts gestionează valoare mare și trebuie să respecte specificații precise. Spre deosebire de testele obișnuite, verificarea formală compară comportamentul sistemului cu o specificație definită matematic.

Diferența este importantă. Testarea clasică întreabă: „Ce se întâmplă dacă Alice depune bani, Bob retrage, iar prețul tokenului se schimbă?” Formal verification întreabă: „Poate exista vreo combinație de pași prin care regula de securitate este încălcată?” Prima metodă caută probleme. A doua încearcă să demonstreze că o clasă întreagă de probleme nu poate apărea.

Asta nu înseamnă că formal verification este un glob de cristal. Ea verifică exact ce i-ai cerut să verifice. Dacă regula este prost formulată, dovada poate fi perfectă și totuși inutilă. E ca și cum ai pune un paznic excelent la ușa din față, dar ai uita că seiful are și o ușă laterală.

În Ethereum există deja instrumente care merg în această direcție. Solidity, limbajul folosit pentru multe contracte inteligente, include SMTChecker, un instrument care încearcă să demonstreze automat proprietăți ale codului și să detecteze probleme precum overflow, împărțirea la zero, cod inaccesibil sau fonduri insuficiente pentru transfer.

AI-ul promite audituri mai rapide, nu securitate prin magie

Până de curând, formal verification era puternică, dar incomodă. Cere specialiști, timp, specificații clare și răbdare. Exact genul de lucruri care lipsesc într-un ecosistem unde unele proiecte se lansează pe repede înainte, cu site lucios, tokenomics ambițios și cod scris sub presiunea pieței.

Aici intră AI-ul. Modelele moderne pot ajuta la citirea codului, propunerea de teste, generarea de specificații și identificarea unor invarianti — adică reguli care trebuie să rămână adevărate indiferent ce se întâmplă în contract. Pentru echipele de securitate, asta poate însemna mai puține ore pierdute pe verificări repetitive și mai mult timp pentru întrebările grele: ce presupuneri face protocolul, ce se întâmplă dacă oracolul greșește, cine poate schimba regulile și unde se află punctul cel mai fragil?

Vitalik Buterin vede potențialul tocmai aici: AI-ul poate genera mult cod, dar codul generat de AI poate avea erori. Formal verification poate deveni filtrul care separă viteza de haos. Potrivit relatărilor CoinDesk și Decrypt, Buterin a argumentat că software-ul verificat matematic ar putea ajuta infrastructura crypto să reziste într-o lume în care atât dezvoltatorii, cât și atacatorii folosesc modele AI tot mai capabile.

Dar promisiunea are limite clare. DeFi nu se sparge doar prin buguri simple. Uneori atacurile vin prin flash loans, manipularea prețurilor, oracole compromise sau decizii de guvernanță exploatate inteligent. Un contract poate fi corect din punct de vedere tehnic și totuși vulnerabil economic.

De aceea, formal verification nu trebuie vândută ca „securitate absolută”. Mai corect ar fi: securitate mai bine definită. În loc să spui vag „acest protocol este sigur”, spui: „aceste proprietăți au fost verificate în aceste condiții, cu aceste ipoteze”. Pentru utilizatori, diferența contează enorm.

Hackerii primesc aceleași superputeri ca apărătorii

Partea incomodă este că inteligența artificială nu alege tabăra bună. Același model care ajută un auditor să găsească o vulnerabilitate poate ajuta și un atacator să o găsească primul. Într-un ecosistem unde codul este adesea public, iar banii sunt lichizi și transferabili instantaneu, viteza devine armă.

AI Security Institute din Marea Britanie a publicat pe 13 mai 2026 o analiză potrivit căreia lungimea sarcinilor cyber pe care modelele AI le pot îndeplini autonom s-a dublat într-un ritm mai rapid decât estimările anterioare. Institutul notează că modele precum Claude Mythos Preview și GPT-5.5 au depășit trendurile estimate anterior, deși evaluările rămân o măsură imperfectă a impactului real.

Într-o evaluare separată, același institut a spus că Claude Mythos Preview a demonstrat progrese în scenarii de tip capture-the-flag și în simulări de atacuri multi-step, în medii controlate și vulnerabile.

AISI subliniază că aceste teste nu trebuie confundate cu performanța garantată împotriva unor sisteme reale bine apărate, dar tendința este suficient de serioasă pentru a conta în planificarea securității.

Pentru piața crypto, mesajul este clar: AI-ul va scurta timpul dintre „există o vulnerabilitate” și „cineva a găsit-o”. Dacă apărătorii îl folosesc pentru audit, atacatorii îl pot folosi pentru scanare. Dacă dezvoltatorii îl folosesc pentru proof generation, hackerii îl pot folosi pentru exploit hunting.

Asta transformă securitatea blockchain într-o cursă de viteză. Nu mai este suficient să repari după atac. Trebuie să demonstrezi înainte de lansare că anumite clase de atacuri nu funcționează.

Crypto merge spre securitate hibridă: AI rapid, oameni suspicioși

Viitorul cel mai probabil nu este o armată de roboți-auditori care înlocuiește complet echipele de securitate. Este un model hibrid. AI-ul face munca rapidă: citește cod, găsește tipare, propune teste, caută vulnerabilități, sugerează dovezi formale. Oamenii fac partea incomodă: decid ce merită verificat, ce ipoteze sunt realiste și unde matematica nu ajunge.

Un protocol serios va avea nevoie în continuare de audituri independente, bug bounty-uri, monitorizare live, guvernanță atentă, controale de acces și planuri clare de intervenție. Formal verification poate deveni un strat esențial al acestei apărări, dar nu întreaga fortăreață.

Pentru proiectele mici, AI-ul poate reduce costurile și poate face verificarea formală mai accesibilă. Pentru proiectele mari, ar putea ridica standardul minim. Dacă un protocol administrează sute de milioane de dolari, simplul mesaj „am trecut prin audit” ar putea să nu mai fie suficient. Investitorii și utilizatorii vor întreba: ce proprietăți au fost demonstrate, ce parte din cod a fost acoperită și ce rămâne neverificat?

Riscul este ca expresia „verificat matematic” să devină noul slogan de marketing, la fel de elastic ca „AI-powered” sau „military-grade security”. O dovadă formală contează doar dacă specificația este clară, ipotezele sunt publice și limitele sunt recunoscute.

AI-ul poate face crypto mai sigur, dar nu pentru că este magic. Îl poate face mai sigur pentru că obligă industria să fie mai precisă. În loc de promisiuni vagi, cere reguli. În loc de încredere, cere demonstrații. În loc de „merge la noi pe testnet”, cere dovada că nu cedează când cineva încearcă să-l rupă.

În final, AI-assisted formal verification este ca un paznic cu calculator de matematică: foarte util, foarte rapid și uneori impresionant. Dar tot oamenii trebuie să-i spună ce seif păzește, ce uși există și ce înseamnă, de fapt, „banii sunt în siguranță”.

Citește și

• Crypto intră în cursa roboților. AI-ul poate sufoca echipele de compliance
• MIT readuce la viață fermoarul cu trei laturi. O idee de acum 40 de ani poate schimba roboții și corturile
• Europa declară război scroll-ului infinit. TikTok și Instagram intră în vizorul Bruxellesului