Peneliti Zcash telah merilis kumpulan lebih dari 2.700 teorema yang diperiksa mesin, dirancang untuk menghilangkan bug pemalsuan yang tidak terdeteksi dalam pembaruan protokol Ironwood yang akan datang. Karya ini, diterbitkan oleh tim di balik mata uang kripto yang berfokus pada privasi, bertujuan untuk membuktikan secara matematis bahwa kode baru tidak dapat dieksploitasi untuk membuat koin palsu tanpa terdeteksi.
Apa yang menjadi target teorema
Teorema-teorema ini berfokus pada Ironwood, sebuah pembaruan yang direncanakan untuk aturan konsensus Zcash. Bug pemalsuan adalah kelas kerentanan yang memungkinkan penyerang mencetak koin dari ketiadaan — sebuah kegagalan katastropik bagi mata uang kripto mana pun. Dengan menggunakan verifikasi formal, peneliti dapat membuktikan secara matematis bahwa properti tertentu berlaku untuk setiap kemungkinan eksekusi kode, bukan hanya mengandalkan audit manual atau pengujian saja.
2.700 teorema tersebut mencakup logika inti dari transaksi terlindungi Ironwood, di mana saldo dan jumlah transaksi dienkripsi. Bukti-bukti ini memeriksa bahwa sistem menegakkan invarian pasokan — artinya tidak ada Zcash yang dapat dibuat melebihi yang diizinkan protokol — bahkan dalam kondisi yang merugikan. Para peneliti mengatakan pendekatan ini menangkap kasus tepi yang mungkin terlewatkan oleh tinjauan kode tradisional.
Mengapa bukti yang diperiksa mesin penting
Verifikasi formal jarang digunakan dalam pengembangan mata uang kripto karena memakan waktu dan memerlukan keahlian khusus. Sebagian besar proyek mengandalkan program bug bounty dan audit manual, yang dapat meninggalkan celah. Zcash telah menggunakan metode formal sebelumnya — untuk pembaruan Sapling asli — tetapi upaya Ironwood adalah penerapan terbesar untuk jaringan tersebut hingga saat ini.
Teorema-teorema ini ditulis dalam bahasa bernama Lean, sebuah asisten pembuktian yang memeriksa setiap langkah penalaran. Jika sebuah teorema lolos, itu berarti properti tersebut dijamin untuk semua masukan. Para peneliti menerbitkan kumpulan bukti lengkap bersama spesifikasi Ironwood, memungkinkan verifikasi independen oleh komunitas.
“Ini tentang memberikan jaminan sekuat mungkin bahwa matematika di balik Ironwood itu benar,” kata tim dalam sebuah pernyataan. “Kami ingin pengguna tahu bahwa pasokan terbukti tetap, bukan hanya diasumsikan.”
Ironwood masih dalam pengembangan. Pekerjaan verifikasi formal adalah tonggak penting, tetapi pembaruan masih harus melalui proses tata kelola Zcash dan diadopsi oleh penambang serta operator node. Para peneliti berencana untuk terus memperluas kumpulan teorema seiring penambahan fitur baru.
Publikasi teorema tidak mengubah apa pun bagi pengguna Zcash saat ini. Jaringan terus berjalan pada protokol yang ada. Namun, karya ini menetapkan preseden untuk bagaimana pembaruan di masa depan dapat divalidasi — dengan kepastian matematis, bukan hanya keyakinan.
Langkah selanjutnya adalah periode peninjauan komunitas, setelah itu kode Ironwood akan diusulkan untuk diaktifkan. Belum ada tanggal yang ditetapkan.
