Vitalik Buterin: AI dan Verifikasi Formal Dapat Mengurangi Risiko Bug di Ethereum

Alat coding berbasis AI kini dapat membantu menulis kode implementasi, menyusun spesifikasi formal, hingga membantu membangun bukti matematis yang diperlukan untuk verifikasi. Ini mengurangi hambatan yang selama ini membuat formal verification hanya digunakan pada proyek kecil atau sangat khusus.

Contoh perubahan kecepatan pengembangan juga terlihat dalam eksperimen terbaru: sebuah proyek pengkodean berbasis AI berhasil menghasilkan prototipe klien Ethereum sekitar 700.000 baris kode hanya dalam beberapa minggu, yang bahkan bisa sinkron dengan mainnet dan mencakup puluhan item roadmap Ethereum.

Namun Buterin menekankan bahwa peningkatan produktivitas ini tidak seharusnya hanya dipakai untuk mempercepat pembangunan fitur. Sebagian besar manfaat AI sebaiknya juga dialokasikan untuk keamanan yang lebih kuat, seperti pengujian yang lebih mendalam dan formal verification.

Area Roadmap Ethereum yang Paling Diuntungkan

Beberapa bagian roadmap Ethereum sangat kompleks dan sensitif terhadap bug, sehingga cocok untuk diverifikasi secara matematis dengan bantuan AI.

ZK‑EVM dan Infrastruktur Zero‑Knowledge

Roadmap jangka panjang Ethereum memberi fokus besar pada teknologi zero‑knowledge (ZK). ZK‑EVM bahkan diperkirakan bisa menjadi metode verifikasi utama jaringan sekitar tahun 2028.

Karena sistem pembuktian kriptografi ini sangat kompleks, verifikasi formal dapat membantu mencegah bug implementasi yang berpotensi berdampak besar.

Keamanan Protokol Inti

Ethereum menempatkan keamanan, desentralisasi, dan kontrol pengguna sebagai prinsip desain utama.

Formal verification dapat membantu memastikan bahwa logika konsensus, implementasi klien, dan komponen kriptografi bekerja tepat seperti yang dimaksudkan oleh protokol.

Infrastruktur Scaling

Dalam roadmap jangka pendek, Ethereum juga berfokus pada peningkatan kapasitas eksekusi dan efisiensi jaringan melalui berbagai upgrade protokol.

Kode tingkat rendah yang digunakan pada bagian sistem yang sangat sensitif terhadap performa sering kali rentan terhadap bug kecil namun berbahaya. Verifikasi formal bisa memberikan jaminan tambahan pada komponen tersebut.

Account Abstraction dan Fitur Privasi

Ethereum juga berencana memperluas dukungan untuk smart‑contract wallet, privasi, dan account abstraction.

Sistem ini melibatkan logika autentikasi, validasi transaksi, dan bukti kriptografi yang kompleks—area yang sangat cocok untuk pendekatan verifikasi formal.

Kriptografi Tahan Komputasi Kuantum

Peneliti Ethereum juga mulai mengeksplorasi kesiapan terhadap post‑quantum cryptography.

Perubahan algoritma kriptografi adalah momen berisiko tinggi bagi sebuah protokol, sehingga implementasi yang diverifikasi secara formal dapat memberikan jaminan keamanan tambahan.

Batasan dan Risiko Meski Dibantu AI

Buterin tidak menganggap AI‑assisted formal verification sebagai solusi ajaib.

Salah satu keterbatasan utama adalah bahwa verifikasi formal hanya dapat membuktikan hal‑hal yang benar‑benar dituliskan dalam spesifikasi. Jika spesifikasinya salah—atau desain ekonomi sistem memiliki kelemahan—maka verifikasi tidak akan mendeteksi masalah tersebut.

Ada juga beberapa tantangan praktis:

• Kode yang dihasilkan AI masih bisa mengandung bug atau implementasi yang tidak lengkap.
• Pengujian manual, audit keamanan, dan peninjauan oleh manusia tetap penting.
• Komponen yang sudah diverifikasi bisa saja berinteraksi dengan bagian sistem lain yang belum diverifikasi.

Buterin juga mengingatkan bahwa implementasi yang dibuat sangat cepat oleh AI sering kali mengandung "bug yang signifikan" dan tetap memerlukan pengujian serta pemeriksaan keamanan yang ketat sebelum benar‑benar digunakan di jaringan produksi.

Gambaran Besarnya

Kemajuan AI tidak hanya membantu pengembang—teknologi ini juga dapat mempermudah penyerang menemukan kerentanan dalam software yang kompleks. Hal itu membuat kebutuhan akan teknik pertahanan yang lebih kuat menjadi semakin mendesak.

Menurut Buterin, infrastruktur blockchain yang mengelola aset bernilai miliaran dolar kemungkinan akan semakin membutuhkan tingkat jaminan seperti ini.

Jika AI mampu mengotomatisasi bagian paling sulit dari formal verification, masa depan pengembangan kripto bisa berubah: sistem penting seperti Ethereum tidak hanya diuji keamanannya, tetapi juga dibuktikan secara matematis aman—setidaknya untuk properti yang dapat didefinisikan secara formal.