Vitalik: Verifikasi formal berbantuan AI berpotensi meningkatkan efisiensi dan keamanan kode secara bersamaan

Foresight News melaporkan bahwa Vitalik Buterin menerbitkan tulisan yang membahas prospek penerapan verifikasi formal di bidang keamanan blockchain. Artikel tersebut menunjukkan bahwa dalam riset pengembangan mutakhir Ethereum tengah muncul paradigma baru, yaitu langsung menggunakan bytecode EVM, assembly, atau Lean untuk menulis kode, serta memverifikasi kebenarannya dengan bukti matematis yang dapat diperiksa secara otomatis di Lean. Peneliti Yoichi Hirai menyebut paradigma ini sebagai "bentuk akhir dari pengembangan perangkat lunak". Vitalik berpendapat bahwa verifikasi formal berbantuan AI berpotensi meningkatkan efisiensi dan keamanan kode secara bersamaan, dan sangat cocok diterapkan pada modul inti keamanan seperti STARK, ZK-EVM, tanda tangan tahan kuantum, dan algoritme konsensus. Namun, artikel tersebut juga menegaskan bahwa verifikasi formal bukanlah solusi sempurna karena masih dapat gagal akibat cakupan pembuktian yang tidak lengkap, spesifikasi yang keliru, atau masalah pada saluran samping perangkat keras. Ke depannya, perangkat lunak kemungkinan akan terbagi menjadi "inti yang aman" dan "pinggiran yang tidak aman", di mana Ethereum akan menjadi salah satu inti keamanan yang penting.