XRPL seeks mathematical proof its new lending market cannot be drained

XRPL developers are using mathematical proofs to test whether the forthcoming lending market can be drained or become insolvent. On Sept. 17, Common Prefix said it was formally verifying XRPL's Lending Protocol with Lean 4. The work is intended to show that the protocol cannot enter states that violate its accounting and safety rules. Version 3.4.0 includes LendingProtocolV1_1. The amendment adds closed-ended lending vaults and cash-basis accounting. The amendment still requires approval through the XRP Ledger's amendment process before taking effect. The lending design lets depositors pool assets for loan brokers to deploy into fixed-term uncollateralized loans. Borrower underwriting and credit assessment occur off-chain. The ledger records loan origination, repayments, and accounting. Closed-ended vaults have subscription, investment, and redemption stages. Depositors can add or withdraw assets during subscription. Both actions are blocked during investment. Withdrawals resume during redemption. The vault timetable is set at creation and cannot be changed later. Cash-basis accounting recognizes interest only when payments arrive. Earlier exploratory verification found vault invariant violations, loan-payment assertion failures, arithmetic rounding errors, and differences between written XLS specifications and their implementation. Common Prefix said the issues were addressed across versions 3.1.3 and 3.2.0. The verification recreates relevant protocol logic in Lean 4 rather than verifying the entire C++ codebase. An oracle compares equivalent inputs across the mathematical model and the production implementation. The guarantees apply only to defined properties and modeled assumptions. The protocol relies on off-chain underwriting and does not currently use automated on-chain collateral and liquidation mechanisms. Loan brokers can provide first-loss capital, but XRPL documentation says this does not eliminate credit risk. Evernorth and VS1.Finance are preparing to use or build around Single Asset Vaults and the Lending Protocol. Validators will ultimately determine whether LendingProtocolV1_1 becomes active.