XRPL tries to mathematically prove its new lending market cannot be drained

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 Prefix said it 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 the work is intended to show that the protocol cannot enter states that violate its accounting and safety rules.

The work has taken on greater significance after xrpld version 3.4.0 shipped this week with LendingProtocolV1_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 design would 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.

Locked capital raises the stakes for XRPL lending

LendingProtocolV1_1 increases 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.

Those changes add more states and transitions that must remain consistent as deposits are accepted, loans are issued, repayments arrive, borrowers default, and vaults eventually reopen for withdrawals.

Common Prefix is using formal verification to test those relationships beyond the scenarios engineers might anticipate in a conventional test suite.

Researchers are not attempting to mathematically verify the entire xrpld C++ codebase. They instead recreate the relevant protocol logic in Lean 4 and define the properties the system is expected to preserve.

An oracle can then run equivalent inputs against the mathematical model and the production implementation, helping identify cases where the two behave differently.

That distinction matters because a mathematical proof is only as strong as the model and assumptions behind it. The process can establish that defined properties hold across the modeled state space, while comparisons with the implementation help test whether the production code continues to match those assumptions.

Earlier proofs already exposed XRPL failures

The approach has already uncovered edge cases that conventional testing missed.

During an exploratory verification phase between February and April, Common Prefix modeled parts of the Lending Protocol and defined invariants the system was expected to maintain.

RippleX said the work uncovered vault invariant violations, loan-payment assertion failures, arithmetic rounding errors, and differences between written XLS specifications and their implementation.

The identified issues were subsequently addressed across xrpld versions 3.1.3 and 3.2.0.

That record gives the current verification effort a practical role before significant depositor capital is placed behind the protocol. Formal methods can challenge assumptions embedded in the lending logic, while developers can still change the implementation before broader adoption.

The problem becomes more complex as native lending interacts with existing ledger functions, including asset transfers, freezes and clawbacks. Each additional interaction expands the number of system states developers must account for.

RippleX has previously argued that this complexity raises the limits of relying solely on functional tests, audits, bug bounties and validator testing.

The stakes are also becoming commercial.

RippleX has identified Evernorth, which is preparing to become a Nasdaq-listed XRP treasury company, and VS1.Finance as among the companies preparing to use or build around Single Asset Vaults and the Lending Protocol, putting more pressure on the underlying accounting rules to behave predictably before institutional capital arrives.

Mathematical proofs still leave credit risk outside the ledger

Even successful verification would leave one of XRPL lending’s largest risks outside the mathematical model: whether borrowers repay.

The protocol relies on off-chain underwriting to determine borrower creditworthiness and does not currently depend on automated on-chain collateral and liquidation mechanisms commonly used in decentralized lending markets.

Loan brokers can supply first-loss capital intended to absorb part of a default before losses reach depositors, but XRPL’s documentation notes that the mechanism does not eliminate credit risk.

Formal verification also cannot prove that every external integration, operational process, or underwriting decision will behave safely. Its guarantees extend only to the properties developers define and the assumptions represented in the model.

That creates two separate layers of assurance for depositors.

The first is whether XRPL’s own accounting machinery behaves consistently across deposits, lending, repayments, and withdrawals. The second is whether loan brokers correctly price and manage borrowers whose obligations remain subject to real-world credit risk.

Common Prefix’s work is focused on strengthening the first. With LendingProtocolV1_1 now distributed in xrpld 3.4.0, validators will ultimately determine whether the amendment becomes active.

Before that happens, developers are trying to establish stronger evidence that the lending machinery itself behaves as specified when real capital, loan brokers, and off-chain credit decisions begin interacting with it.