Common Prefix 正式驗證 $XRP Ledger 借貸協議，以數學方式證明其無法被抽乾、資不抵債或違反規則。 這項工作聚焦於透過 XLS-66 引入的借貸協議。Common Prefix 在六部分系列文章中解釋了其方法，包括為何選擇 Lean 4 進行驗證。 Common Prefix 表示，形式化驗證超越了常規軟體測試，透過數學證明系統在所有可能情況下都能正確運作。 XRP Ledger 驗證節點 Vet（又稱 Hussein Zangana）表示，形式化驗證已應用於高風險系統，例如軍事技術、空中交通軟體、飛行控制系統和核電廠。 他解釋說，這種方法透過數學證明系統在所有可能輸入下均保持有效，而不僅限於開發者測試過的情況。 Common Prefix 評估了多種工具，包括 Dafny、Lean 4、TLA+ 和 P。團隊認為 TLA+ 和 P 不適合回答有關借貸協議的特定問題。 選擇 Lean 4 的原因之一是它不依賴 SMT 求解器。Common Prefix 發現 Dafny 的求解器在處理驗證所需的複雜算術時，有時會超時。Lean 需要更多手動工作，但這也讓開發者更容易發現和修復錯誤。#Ripple https://t.co/s0YcQ4KAWX