Binubuo ng Common Prefix ang pormal na pag-verify sa $XRP Ledger Lending Protocol upang matematikal na patunayan na ito ay hindi maaaring mapawalan, maging insolvent, o lumabag sa mga alituntunin nito. Ang trabaho ay nakatuon sa Lending Protocol na ipinakilala sa pamamagitan ng XLS-66. Ipinaliwanag ng Common Prefix ang kanilang pamamaraan sa isang anim-kasapi na serye, kabilang ang dahilan kung bakit nila pinili ang Lean 4 para sa proseso ng pag-verify. Sinabi ng Common Prefix na ang pormal na pag-verify ay lumalampas sa karaniwang pagsubok ng software sa pamamagitan ng paggamit ng matematika upang patunayan na ang isang sistema ay gumagana nang tama sa lahat ng posibleng sitwasyon. Si Vet, isang validator ng XRP Ledger na kilala rin bilang Hussein Zangana, ay sinabi na ang pormal na pag-verify ay ginagamit na sa mga mataas na panganib na sistema tulad ng militar na teknolohiya, software ng air traffic, mga kontrol sa paglipad, at mga nukleyar na pwersa plant. Ipinaliwanag niya na ang pamamaraang ito ay gumagamit ng matematika upang ipakita na ang isang sistema ay nananatiling wasto sa lahat ng posibleng input, hindi lamang sa mga sitwasyon na sinubok ng mga developer. Isinasaalang-alang ng Common Prefix ang ilang mga kasangkapan, kabilang ang Dafny, Lean 4, TLA+, at P. Pumili ang koponan na ang TLA+ at P ay hindi angkop para sa mga partikular na tanong na kailangan nilang sagutin tungkol sa lending protocol. Isang dahilan kung bakit pinili nila ang Lean 4 ay dahil hindi ito nakabatay sa isang SMT solver. Natuklasan ng Common Prefix na ang solver ng Dafny ay minsan ay maaaring mag-time out habang sinusolusyon ang mga kumplikadong aritmetika na kailangan para sa pag-verify. Kinakailangan ng Lean ng higit pang gawain mula sa kamay, ngunit ito ay nagiging mas madaling hanapin at ayusin ng mga developer ang mga error. #Ripple https://t.co/s0YcQ4KAWX