XRPL's Lending Protocol Gets a Lean 4 Math Proof as xrpld 3.4.0 Ships
Common Prefix is formally verifying XRPL's Lending Protocol in Lean 4, days after xrpld 3.4.0 shipped with closed-ended vaults and cash-basis accounting. The math can prove the books balance. It can't prove borrowers will pay.
Common Prefix says it's formally verifying the XRP Ledger's Lending Protocol in Lean 4, a theorem-proving language built to check whether software holds up across every possible system state. The Sept. 17 announcement is narrow on purpose: prove the protocol can't slip into states that violate its own accounting and safety rules.
Timing is the key detail. xrpld version 3.4.0 shipped this week with LendingProtocolV1_1, an amendment that adds closed-ended lending vaults and cash-basis accounting. It's in the server software but not live. Validators still have to approve it.
The design works like this. Vaults run through three stages, subscription, investment, redemption. Depositors can move assets in and out during subscription. Once the investment period starts, both doors shut. The timeline gets set when the vault is created and can't be changed afterward. Cash-basis accounting also means interest is recognized only as payments arrive, not when a loan originates.
That's a meaningful shift. Under the earlier design, a vault could book interest income before a borrower paid a cent, which risks inflating share values on money that never shows up.
And this isn't hypothetical. Between February and April, Common Prefix modeled parts of the protocol and found vault invariant violations, loan-payment assertion failures, rounding errors, and mismatches between the written XLS specs and the implementation. Those got patched across xrpld 3.1.3 and 3.2.0. The precedent here's important. Formal methods caught what a conventional test suite missed.
Native lending also has to interact with transfers, freezes, and clawbacks, and every added interaction multiplies the state space developers have to account for.
But math has a ceiling. It can't verify that borrowers repay. XRPL lending leans on off-chain underwriting for uncollateralized, fixed-term loans, with no on-chain collateral or automated liquidation. Brokers can post first-loss capital, though XRPL's own documentation concedes that doesn't wipe out credit risk. So depositors get two layers of assurance, and only one of them is provable.
Reading between the lines, the commercial pressure is arriving faster than the proofs. RippleX has flagged Evernorth, the XRP treasury company heading to a Nasdaq listing, and VS1.Finance as early users of Single Asset Vaults. Institutional capital won't sit behind a vault it can't audit, and that's the deadline that matters.