XRPL tries to mathematically prove its new lending market cannot be drained
Common Prefix is using Lean 4 to verify XRPL’s native lending system after earlier proofs uncovered bugs conventional testing missed.
XRP Ledger (XRPL) developers are using mathematical proofs to test whether the network’s forthcoming lending market can be drained or become insolvent.
On Sept. 17, protocol research firm Common Prefixsaidit is formally verifying XRPL’s Lending Protocol with Lean 4, a theorem-proving language designed to establish whether software satisfies defined mathematical properties across possible system states.
The firm said theworkis intended to show that the protocol cannot enter states that violate its accounting and safety rules.
The work has taken on greater significance afterxrpldversion 3. 4. 0 shipped this week with Lending ProtocolV1_1, an amendment that introduces closed-ended lending vaults and cash-basis accounting. The amendment is included in the server software but still requires approval through the XRP Ledger’s amendment process before taking effect.
XRPL’s lending designwould allow depositors to pool assets that loan brokers can deploy into fixed-term, uncollateralized loans. Borrower underwriting and credit assessment happen off-chain, while the ledger records loan origination, repayments, and accounting.
That puts a premium on getting the protocol’s internal bookkeeping right. Errors involving vault balances, loan payments, or share calculations could affect pooled depositor funds rather than an isolated application.
Lending ProtocolV1_1increases the consequences of accounting failures because depositor assets can remain committed through a predetermined investment period.
Closed-ended vaults move through three stages: subscription, investment, and redemption. Depositors can add or withdraw assets during the subscription phase, but both actions are blocked once the vault enters its investment period and the capital becomes available for lending. Withdrawals resume when the vault reaches redemption.
The timetable is set when the vault is created and cannot be changed later, giving participants advance visibility into how long their capital may remain committed.
Version 3. 4. 0 also changes how new vaults recognize interest income.
Under the earlier design, scheduled interest could be recorded as income when a loan was originated, even before the borrower made those payments. Cash-basis accounting instead recognizes interest only as payments arrive, reducing the risk that vault-share values reflect income not yet received.
출처: CryptoSlate