- Ethereum telah menamakan teknologi yang boleh memperkuat keselamatan kontrak pintar di era AI.
- Menurut seorang pembangun Vyper, pengesahan formal menjadi sangat penting.
- Ia membantu mencari ralat yang tidak dikesan oleh ujian.
Pasukan rangkaian ethereum menerbitkan siri tulisan tetamu daripada pembangun utama Vyper dengan nama samaran big_tech_sux, yang berfokus pada peranan pengesahan formal di era pembangunan AI yang pesat.
0/ Semasa sistem AI menjadi lebih kuat, pengesahan formal – yang merupakan disiplin menggunakan matematik untuk membuktikan kebenaran program komputer – menunjukkan janji yang semakin meningkat.
— Ethereum (@ethereum) 5 Ogos 2026
Sebuah thread tetamu oleh @big_tech_sux, pembangun utama @vyperlangpic.twitter.com/3T6H76AVrL
Penulis berhujah bahawa kemajuan dalam LLM membuat bukti matematik bagi kebetulan program menjadi lebih boleh diakses, dan bagi kontrak pintar yang menguruskan berbilion dolar, pengesahan formal perlahan-lahan menjadi keperluan.
AI Mengubah Pendekatan Terhadap Pengesahan Perisian
Rangkaian postingan tersebut menjelaskan bahawa pengesahan formal ialah kaedah matematik yang membolehkan pembuktian bahawa program berfungsi dengan betul di sepanjang semua senario pelaksanaan yang mungkin, bukan hanya yang dicakup oleh ujian.
Sebagai contoh, penulis merujuk kepada fungsi f(x) = x/2, di mana ia boleh dibuktikan secara matematik bahawa hasilnya tidak akan melebihi nilai input.
Menurutnya, metodologi ini boleh mengesan ralat yang sangat jarang berlaku, yang hampir mustahil untuk dikesan melalui pengujian konvensional.
“Pengesahan formal boleh menangkap 1 dalam 1 kuadriliun kes tepi yang tidak akan pernah timbul semasa pengujian – dan kes tepi itulah yang boleh menyebabkan kegagalan bencana,” catat penulis.
Pada masa yang sama, beliau mengakui bahawa sehingga baru-baru ini, penggunaan pendekatan ini memerlukan pasukan pakar yang besar yang membina model matematik bagi program dan menjalankan bukti yang kompleks.
Dalam pandangan pengembang, LLM moden secara signifikan menyederhanakan proses ini seiring kita semakin mendekati AGI.
Pada masa yang sama, penulis menekankan bahawa walaupun dengan AI, pengesahan formal tetap merupakan proses yang kompleks dan memerlukan sumber yang banyak. Secara khusus, penukaran kod sumber kepada model formal boleh memperkenalkan ketidaktepatan yang mempengaruhi kebolehpercayaan keputusan.
Perkembangan AI Mengubah Keseimbangan Antara Serangan dan Pertahanan
Karya itu mencatat bahawa pembangunan kecerdasan buatan secara serentak meningkatkan keberkesanan kedua-dua pihak pertahanan dan penyerang.
Penulis mengingat satu insiden di mana model OpenAI yang belum dirilis berjaya menemui kelemahan zero-day yang membolehkan melangkau beberapa lapisan perlindungan.
Dalam konteks ini, pengesahan formal, menurut penulis, memungkinkan peralihan keuntungan ke pihak pertahanan.
“Sementara penyerang hanya perlu mencari satu urutan input yang membolehkan mereka menembus sistem, pihak pertahanan boleh menggunakan pengesahan formal untuk membuktikan ketahanan terhadap semua input,” katanya menekankan.
Itu sebabnya, untuk perisian kritikal misi — termasuk kontrak pintar yang menguruskan bilion dolar dana pengguna — pengesahan formal menjadi “bukan pilihan, tetapi prasyarat yang perlu”.
Perlu diperhatikan bahawa ini meneruskan perbincangan sebelumnya dimulakan oleh salah seorang penemu ethereum, Vitalik Buterin, mengenai penggunaan AI untuk pengesahan formal kod.
Mesej Ethereum Explained How AI Changes Approach to Smart Contract Security pertama kali muncul di INCRYPTED.