Common Prefix to formally verify XRPL lending protocol with Lean 4

Protocol research firm Common Prefix announced on Sept. 17 that it is formally verifying the XRP Ledger’s Lending Protocol using Lean 4. As reported by CryptoSlate, the aim is to demonstrate that the system cannot reach configurations that break its accounting and safety constraints.

xrpld version 3.4.0 shipped this week with LendingProtocolV1_1, adding closed-ended lending vaults and cash-basis accounting. These vaults progress through subscription, investment, and redemption phases, with deposits and withdrawals prohibited during the investment period.

From February to April, Common Prefix conducted an exploratory verification phase, modeling specific parts of the protocol. RippleX stated that this effort revealed violations of vault invariants, assertion failures in loan payments, and arithmetic rounding errors. Fixes for these issues were incorporated into xrpld versions 3.1.3 and 3.2.0.

RippleX named Evernorth and VS1.Finance as firms ready to utilize or develop on the Single Asset Vaults and Lending Protocol. Evernorth is in the process of becoming a Nasdaq-listed XRP treasury company.

Common Prefix is not mathematically verifying the entire xrpld C++ codebase. Instead, researchers reimplement the relevant protocol logic in Lean 4 and specify the invariants the system must maintain. An oracle subsequently executes comparable inputs against both the mathematical model and the live implementation.

The amendment is present in the server software but awaits ratification via the XRP Ledger’s amendment process before becoming active.