Di KTT Cendekiawan Web3, Profesor Yale Pertama Kali Memperkenalkan Model LiDO

Pada Konferensi Cendekiawan Web3 2025, Profesor Zhao Zhong dari Departemen Ilmu Komputer Universitas Yale memberikan pidato utama berjudul "Keamanan dan Bukti Aktivitas Protokol Konsensus Berbasis Refinement: LiDO dan Perluasannya", yang secara resmi memperkenalkan model LiDO dan kerangka perluasan LiDO-DAG yang dikembangkan oleh timnya. Hasil terobosan ini bertujuan untuk menyediakan bukti keamanan dan aktivitas yang dapat diverifikasi secara mekanis untuk protokol konsensus Byzantine Fault Tolerant (BFT) yang kompleks, meletakkan fondasi teknologi untuk keandalan dan pengembangan skala Web3.

Profesor Shao Zhong menunjukkan bahwa meskipun protokol konsensus yang ada digunakan secara luas, tetapi karena kompleksitas implementasinya, sering kali menyembunyikan kerentanan yang potensial. Untuk mengatasi masalah ini, model LiDO secara inovatif mengusulkan kerangka verifikasi terperinci tiga lapis:

1. Lapisan Abstraksi Keamanan: Memetakan protokol ke dalam mesin status linier, memastikan konsistensi log (keamanan);
2. Lapisan Jaminan Aktivitas: Memperkenalkan mekanisme "Pacemaker" untuk memecahkan masalah keterlambatan jaringan melalui siaran waktu habis dan sinkronisasi putaran;
3. Lapisan Ekstensi DAG: Mendukung protokol DAG yang muncul, mewujudkan verifikasi efisien tanpa pemimpin.

Saat ini, LiDO telah berhasil diterapkan pada protokol tingkat industri Jolteon (BFT dua tahap) dan beberapa protokol DAG, menyelesaikan lebih dari sepuluh ribu baris kode Coq untuk pembuktian mekanis, dengan jumlah kode untuk verifikasi keamanan dan aktivasi masing-masing mencapai 4000 baris dan 1700 baris. Profesor Shao Zhong dalam pidatonya menunjukkan: "Saat ini, protokol konsensus PoS umumnya menghadapi kesulitan untuk mendapatkan keamanan, aktivasi, dan desentralisasi secara bersamaan. Model LiDO adalah solusi desain sistematis yang diajukan untuk memecahkan masalah ini."

CertiKOS yang dikembangkan oleh Profesor Shao Zhong dan timnya adalah sistem operasi "tanpa kerentanan" pertama di dunia yang telah melalui verifikasi formal, yang dijuluki sebagai "tonggak sejarah keamanan sistem fisik jaringan". Prestasi ini tidak hanya menetapkan dasar teknisnya di bidang keamanan sistem, tetapi juga mencerminkan akumulasi mendalam yang dimilikinya. Dalam beberapa tahun terakhir, Profesor Shao Zhong telah fokus pada keamanan blockchain, dan pada tahun 2017, bersama muridnya Profesor Gu Ronghui, mereka memperkenalkan teknologi verifikasi formal untuk menjamin keamanan kontrak pintar dan protokol on-chain, melindungi keamanan aset kripto senilai miliaran dolar.

LiDO saat ini telah menyelesaikan desain model dan verifikasi formal, dan mulai mengeksplorasi kemungkinan integrasi dengan blockchain utama dan protokol terdesentralisasi. Profesor Shao Zhong menyatakan bahwa mereka berkomitmen untuk memverifikasi mekanisme kunci dalam Web3.0, untuk menyediakan produk dan layanan sepanjang siklus, guna mendukung strategi pengembangan jangka panjang untuk perusahaan dan ekosistem Web3. Di akhir pidato, Profesor Shao Zhong menekankan: "Tumpukan protokol jaringan yang dapat dipercaya, aman, dan dapat diverifikasi, akan menjadi jalur kunci menuju masa depan yang benar-benar terdesentralisasi."