Sonic Labs Meluncurkan Pustaka Verifikasi Formal untuk Protokol Konsensus DAG

Tim di balik blockchain Layer 1 berkinerja tinggi Sonic, Lab Sonic memperkenalkan pustaka verifikasi formal yang dirancang untuk meningkatkan keamanan dalam protokol konsensus berbasis DAG. Dipimpin oleh Kepala Riset Dr. Bernhard Scholz, pustaka ini bertujuan untuk memberikan bukti matematis tentang keamanan untuk blockchain Directed Acyclic Graph (DAG), termasuk jaringan Sonic yang kompatibel dengan EVM.

Dikembangkan melalui kerja sama dengan para peneliti dari University of Sydney dan INRIA, pustaka sumber terbuka ini dibangun menggunakan asisten pembuktian TLA+. Pustaka ini menawarkan kerangka kerja modular dan dapat digunakan kembali yang menyederhanakan proses pemodelan dan verifikasi mekanisme konsensus berdasarkan arsitektur DAG.

Pustaka verifikasi ini menampilkan bukti formal untuk beberapa protokol berbasis DAG yang ada, seperti DAG-Rider, Cordial Miner, Bullshark, Hashgraph, dan Aleph. Protokol milik Sonic juga telah diverifikasi sebagai turunan dalam kerangka kerja ini. Penelitian ini pertama kali dipresentasikan pada konferensi NASA Formal Methods 2025, yang diadakan di Williamsburg, Virginia, dari tanggal 11 hingga 13 Juni, dan merupakan kemajuan penting dalam standar verifikasi blockchain.

"Dalam blockchain, kegagalan keamanan sering kali berasal dari asumsi yang tidak teruji hingga terlambat," kata Dr. Bernhard Scholz, Kepala Riset di Sonic Labs, dalam pernyataan tertulis. "Dengan pustaka ini, kami beralih dari harapan ke bukti, menawarkan alat untuk memverifikasi dengan kepastian matematis bahwa protokol akan berfungsi dengan aman dalam semua kondisi. Tujuan kami adalah membuat verifikasi formal dapat diakses oleh setiap pengembang protokol," tambahnya.

Seiring Melonjaknya Nilai Blockchain, Sonic Labs Meluncurkan Kerangka Verifikasi Formal untuk Memastikan Keamanan dan Keandalan Protokol

Karena nilai yang diamankan oleh jaringan blockchain terus tumbuh, dampak potensial dari kerentanan dalam protokol konsensus menjadi semakin signifikan, dengan risiko termasuk pengeluaran ganda dan status buku besar yang tidak konsisten. Pengujian konvensional dan audit kode terbatas dalam kemampuannya untuk menjamin sistem bebas bug. Sebagai tanggapan, metode verifikasi formal telah diterapkan oleh Lab Sonic , memanfaatkan bukti matematis untuk mengonfirmasi keamanan protokol di semua kemungkinan kondisi.

Pendekatan ini tidak hanya memvalidasi protokol konsensus yang ada tetapi juga membantu pengembang yang merancang model berbasis Directed Acyclic Graph baru atau mengadaptasi model yang ada saat ini. Metode ini saat ini sedang diimplementasikan untuk memverifikasi secara formal bahwa blockchain Sonic tidak dapat menunjukkan perilaku yang tidak aman, menetapkan keandalan protokol melalui validasi matematis.

Dengan menyediakan pustaka verifikasi secara terbuka, inisiatif ini menyediakan sumber daya bagi pengembang blockchain untuk membangun sistem yang terbukti aman. Hal ini diharapkan dapat meningkatkan ketahanan ekosistem terdesentralisasi secara keseluruhan dan mengurangi permintaan sumber daya yang biasanya terkait dengan verifikasi protokol konsensus.