Ko-founder ethereum Vitalik Buterin mengusulkan bahasa pemrograman baru. Bahasa tersebut akan dikompilasi langsung ke Lean atau HOL, asisten bukti formal lainnya.
Gagasan ini menargetkan kesenjangan spesifik dalam cara orang membaca output AI. Kecerdasan buatan semakin sering menghasilkan blok-blok besar bukti otomatis, seringkali lebih cepat daripada tim manusia mana pun yang bisa menulisnya secara manual. Sedikit pembaca yang dapat dengan cepat memastikan apa yang sebenarnya dibuktikan oleh bukti-bukti tersebut.
Sebuah Bahasa yang Dibuat Hanya untuk Pemeriksa AI
Lean adalah alat bantu bukti, perangkat lunak yang digunakan oleh matematikawan dan insinyur untuk menulis bukti yang dapat diperiksa komputer baris demi baris. Peneliti ethereum sudah menggunakannya untuk memverifikasi kode kriptografi dan logika konsensus. Alat bantu bukti telah ada selama hampir 60 tahun, namun bidang ini tetap menjadi kegiatan yang sempit.
Dalam postingannya, Buterin berargumen bahwa langkah-langkah internal suatu bukti hanya memiliki satu persyaratan. Persyaratan itu adalah kebenaran matematis, tidak lebih. Pembaca tidak pernah memeriksa mesin tersebut secara langsung. Definisi dan teorema bekerja berbeda, karena manusia membaca bagian-bagian itu untuk memahami apa yang sebenarnya dijamin oleh sebuah perangkat lunak.
Buterin membahas pemisahan terkait dalam postingan blog Mei. Di sana, bukti matematis menunjukkan bahwa kode tingkat rendah yang efisien sesuai dengan spesifikasi terpisah yang mudah dibaca, sehingga satu audit mencakup kedua versi sekaligus.
Waktunya juga selaras dengan upaya pembaruan Ethereum sendiri, yang memiliki nama panggilan terpisah, Lean Ethereum roadmap. Para peneliti saat ini sedang membangun formally verified ZK-EVM, versi mesin virtual Ethereum (EVM) yang dapat dibuktikan dengan zero-knowledge, menggunakan metode yang sebanding.
AI Menulis Bukti, Manusia Memeriksa Klaim
Model bahasa besar sudah dapat menulis bukti Lean yang dapat digunakan. Buterin menyebut Claude dan Deepseek 4 Pro sebagai alat yang mampu, bersama Leanstral, model yang lebih kecil yang disesuaikan khusus untuk Lean. Salah satu contoh proyek adalah evm-asm, implementasi EVM yang diverifikasi terhadap referensi yang mudah dibaca. Kemampuan ini mencerminkan keterampilan penalaran yang ditunjukkan pengembang dalam tantangan AI Buterin terbaru challenge. Para pengujinya menyelesaikan tantangan tersebut dalam hitungan jam.
Staking melampaui sekadar kenyamanan, bagaimanapun. Para peneliti keamanan telah melacak peningkatan upaya eksploitasi yang dibantu AI tahun ini. Kode yang diverifikasi secara formal menawarkan satu pertahanan terhadap tren tersebut. Bahasa spesifikasi yang lebih ramah akan memungkinkan pengembang untuk mengaudit klaim tanpa harus menyelami bukti di sekitarnya.
Di Luar Lingkaran Riset Ethereum
Buterin terus menguji ide-ide ini secara publik, baru-baru ini ia mendemonstrasikan billboard anonim yang dibangun dengan zero-knowledge proof. Demonstrasi tersebut menunjukkan bagaimana klaim yang dapat diverifikasi dapat berpindah dari repositori penelitian ke produk yang berfungsi. Para peneliti juga mulai secara formal memverifikasi klien konsensus dalam Lean untuk mendeteksi bug sejak dini.
Namun, arahnya mengikuti pola yang sudah dikenal: pisahkan kode cepat dari klaim yang mudah dibaca, lalu buktikan bahwa keduanya sesuai.
Belum ada prototipe bahasa baru, dan Buterin membiarkan sintaksnya terbuka. Para pengembang mungkin akan menyepakati satu standar bersama, atau justru menerima beberapa dialek yang tidak kompatibel. Pilihan itu bisa menentukan seberapa cepat kode yang diverifikasi AI mencapai sistem produksi.