Common Prefix sedang secara rasmi mengesahkan Protokol Peminjaman $XRP Ledger untuk membuktikan secara matematik bahawa ia tidak boleh dikosongkan, menjadi insolven, atau melanggar peraturannya. Kerja ini berfokus pada Protokol Peminjaman yang diperkenalkan melalui XLS-66. Common Prefix menjelaskan pendekatannya dalam siri enam bahagian, termasuk sebab ia memilih Lean 4 untuk proses pengesahan. Common Prefix menyatakan bahawa pengesahan formal melampaui ujian perisian biasa dengan menggunakan matematik untuk membuktikan bahawa sistem berfungsi dengan betul dalam semua situasi yang mungkin. Pengesah XRP Ledger, Vet, juga dikenali sebagai Hussein Zangana, berkata pengesahan formal sudah digunakan dalam sistem berisiko tinggi seperti teknologi tentera, perisian trafik udara, kawalan penerbangan, dan loji kuasa nuklear. Beliau menjelaskan bahawa pendekatan ini menggunakan matematik untuk menunjukkan bahawa sistem tetap sah di sepanjang semua input yang mungkin, bukan hanya situasi yang telah diuji oleh pembangun. Common Prefix mempertimbangkan beberapa alat, termasuk Dafny, Lean 4, TLA+, dan P. Pasukan memutuskan bahawa TLA+ dan P tidak sesuai untuk soalan spesifik yang perlu dijawab mengenai protokol peminjaman. Salah satu sebab ia memilih Lean 4 ialah ia tidak bergantung pada penyelesaian SMT. Common Prefix mendapati bahawa penyelesaian Dafny kadang-kadang boleh habis tempoh apabila menangani aritmetik kompleks yang diperlukan untuk pengesahan. Lean memerlukan lebih banyak kerja secara manual, tetapi ini juga menjadikan ralat lebih mudah ditemui dan diperbaiki oleh pembangun. #Ripple https://t.co/s0YcQ4KAWX