XRPL貸款協議啟動 Lean 4 形式驗證

XRP Ledger（XRPL）新貸款協議已啟動數學驗證，確認資金流與會計規則是否符合定義，但這不代表借款人違約或信用風險將因此消失。

協議研究公司 Common Prefix 於 9 月 17 日表示，正以形式化證明語言 Lean 4 驗證 XRPL 貸款協議。驗證範圍包括存款、借貸、還款與贖回流程是否違反既定的會計與安全規則。

形式驗證不同於執行部分情境的一般測試。研究團隊並未直接證明完整的 xrpld C++ 程式碼，而是以 Lean 4 重現核心邏輯，並定義模型必須遵守的屬性。

接著，研究團隊會對模型與實際實作套用相同輸入，確認兩者結果是否一致。因此，證明範圍僅限於模型涵蓋的狀態與研究團隊設定的假設。Common Prefix 在公開資料中說明了單一資產金庫與貸款協議的形式驗證工作。

這項工作不代表 XRPL 貸款功能已在主網全面啟用。Ripple 開源文件將 LendingProtocolV1_1 說明為引入封閉式金庫與現金制會計的 amendment，實際採用仍需要主網投票與共識程序。

XRPLF 公開的 xrpld 3.4.0 版本紀錄包含 LendingProtocolV1_1 相關功能。不過，功能寫入程式碼與該 amendment 在帳本上啟用，是兩個不同程序。

LendingProtocolV1_1 的金庫分為認購、投資與贖回三個階段。認購階段可存入和提取資金；投資階段資金會被鎖定並用於新貸款；貸款到期並完成還款後，存款人可在贖回階段將持份兌換為現金。

XRPL 官方單一資產金庫文件列出各階段的交易條件。這套結構會把存款何時投入貸款、何時可以贖回，反映在帳本狀態中。

會計方式也有所調整。既有結構會在貸款發放後立即將預定利息列為收益；LendingProtocolV1_1 則採用現金制會計，在實際收到還款時才確認利息。

這種方式可降低尚未收到的利息提前計入金庫資產與持份價值的問題。但即使會計處理規則更精細，也不會消除借款人無法還款的風險。

在先前的驗證過程中，研究團隊發現金庫不變量違反、貸款還款驗證錯誤、算術四捨五入問題，以及 XLS 規格與實際實作之間的差異。RippleX 曾在開發者貼文中表示，相關修正已納入 xrpld 3.1.3 與 3.2.0。

這些發現顯示，形式驗證不只是上線前檢查，也能用來找出實作與規格之間的差異。另一方面，未納入驗證模型的狀態，或研究團隊未設定的假設，並不在證明範圍內。

XRPL 貸款協議的信用風險仍須另行處理。XRPL 貸款協議文件說明，相關機制不採用抵押品與自動清算，而是在鏈下進行借款人信用評估與承保審查。

貸款經紀商提供的優先損失承擔資本或可吸收部分損失，但無法消除借款人違約本身。因此，這次驗證確認的重點不是借款人是否一定還款，而是帳本內的存款、借貸、還款與贖回會計，是否依照既定規則運作。

XRPL 機構貸款基礎設施的討論先前也曾由本刊報導。此次形式驗證，是在這類貸款功能實際套用至帳本前，檢查會計與狀態轉換穩定性的階段。

在主網啟用狀態與最終驗證範圍確定前，仍難以認定 XRPL 貸款市場的安全性已獲證明。後續市場將關注 LendingProtocolV1_1 amendment 是否獲得批准，以及鏈下貸款審查架構的具體安排。