Common Prefix secara resmi memverifikasi Protokol Pinjaman #XRP Ledger Lending Protocol untuk membuktikan secara matematis bahwa protokol tersebut tidak dapat dikuras, menjadi tidak mampu membayar (insolvent), atau melanggar aturan-aturannya.
Pekerjaan ini berfokus pada Protokol Pinjaman yang diperkenalkan melalui XLS-66. Common Prefix menjelaskan pendekatannya dalam rangkaian enam bagian, termasuk alasan memilih Lean 4 untuk proses verifikasi.
Common Prefix mengatakan bahwa verifikasi formal melampaui pengujian perangkat lunak biasa dengan menggunakan matematika untuk membuktikan bahwa sebuah sistem bekerja dengan benar dalam semua kemungkinan situasi.
Validator XRP Ledger, yang juga dikenal sebagai Hussein Zangana, mengatakan bahwa verifikasi formal sudah digunakan dalam sistem berisiko tinggi seperti teknologi militer, perangkat lunak lalu lintas udara, kontrol penerbangan, dan pembangkit listrik tenaga nuklir.
Ia menjelaskan bahwa pendekatan ini memakai matematika untuk menunjukkan bahwa sebuah sistem tetap valid di seluruh kemungkinan masukan, bukan hanya situasi yang telah diuji oleh pengembang.
Common Prefix mempertimbangkan beberapa alat, termasuk Dafny, Lean 4, TLA+, dan P. Tim memutuskan bahwa TLA+ dan P tidak cocok untuk pertanyaan spesifik yang perlu dijawab terkait protokol pinjaman.
Salah satu alasan memilih Lean 4 adalah karena alat tersebut tidak bergantung pada SMT solver. Common Prefix menemukan bahwa solver Dafny terkadang bisa mengalami waktu habis (timeout) saat menangani aritmetika kompleks yang diperlukan untuk verifikasi. Lean memang membutuhkan lebih banyak pekerjaan secara manual, tetapi hal itu juga memudahkan pengembang menemukan dan memperbaiki kesalahan.
#CryptoNewsCommunity
Pekerjaan ini berfokus pada Protokol Pinjaman yang diperkenalkan melalui XLS-66. Common Prefix menjelaskan pendekatannya dalam rangkaian enam bagian, termasuk alasan memilih Lean 4 untuk proses verifikasi.
Common Prefix mengatakan bahwa verifikasi formal melampaui pengujian perangkat lunak biasa dengan menggunakan matematika untuk membuktikan bahwa sebuah sistem bekerja dengan benar dalam semua kemungkinan situasi.
Validator XRP Ledger, yang juga dikenal sebagai Hussein Zangana, mengatakan bahwa verifikasi formal sudah digunakan dalam sistem berisiko tinggi seperti teknologi militer, perangkat lunak lalu lintas udara, kontrol penerbangan, dan pembangkit listrik tenaga nuklir.
Ia menjelaskan bahwa pendekatan ini memakai matematika untuk menunjukkan bahwa sebuah sistem tetap valid di seluruh kemungkinan masukan, bukan hanya situasi yang telah diuji oleh pengembang.
Common Prefix mempertimbangkan beberapa alat, termasuk Dafny, Lean 4, TLA+, dan P. Tim memutuskan bahwa TLA+ dan P tidak cocok untuk pertanyaan spesifik yang perlu dijawab terkait protokol pinjaman.
Salah satu alasan memilih Lean 4 adalah karena alat tersebut tidak bergantung pada SMT solver. Common Prefix menemukan bahwa solver Dafny terkadang bisa mengalami waktu habis (timeout) saat menangani aritmetika kompleks yang diperlukan untuk verifikasi. Lean memang membutuhkan lebih banyak pekerjaan secara manual, tetapi hal itu juga memudahkan pengembang menemukan dan memperbaiki kesalahan.
#CryptoNewsCommunity