Common Prefix secara resmi memverifikasi Protokol Peminjaman $XRP Ledger untuk membuktikan secara matematis bahwa protokol tersebut tidak dapat dikosongkan, menjadi tidak solvable, atau melanggar aturannya. Pekerjaan ini berfokus pada Protokol Peminjaman yang diperkenalkan melalui XLS-66. Common Prefix menjelaskan pendekatannya dalam serangkaian enam bagian, termasuk alasan memilih Lean 4 untuk proses verifikasi. Common Prefix menyatakan bahwa verifikasi formal melampaui pengujian perangkat lunak biasa dengan menggunakan matematika untuk membuktikan bahwa sistem berfungsi dengan benar dalam semua kemungkinan situasi. Validator XRP Ledger, Vet, yang juga dikenal sebagai Hussein Zangana, mengatakan verifikasi formal sudah digunakan dalam sistem berisiko tinggi seperti teknologi militer, perangkat lunak lalu lintas udara, kendali penerbangan, dan pembangkit listrik tenaga nuklir. Ia menjelaskan bahwa pendekatan ini menggunakan matematika untuk menunjukkan bahwa sistem tetap valid di semua kemungkinan masukan, bukan hanya dalam 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 mengenai protokol peminjaman. Salah satu alasan memilih Lean 4 adalah karena alat ini tidak bergantung pada SMT solver. Common Prefix menemukan bahwa solver Dafny terkadang mengalami timeout saat menangani aritmetika kompleks yang dibutuhkan untuk verifikasi. Lean memerlukan lebih banyak pekerjaan manual, tetapi hal ini juga membuat kesalahan lebih mudah ditemukan dan diperbaiki oleh pengembang. #Ripple https://t.co/s0YcQ4KAWX