Common Prefix is formally verifying the XRP Ledger’s Lending Protocol in Lean 4 to test whether its accounting and safety rules hold across possible system states. The effort follows the release of xrpld 3.4.0, which includes LendingProtocolV1_1, an amendment introducing closed-ended lending vaults and cash-basis accounting that still requires approval through the XRP Ledger amendment process. The design lets depositors pool assets for loan brokers to deploy into fixed-term, uncollateralized loans, with underwriting and credit assessment conducted off-chain. Earlier exploratory work between February and April identified vault invariant violations, loan-payment assertion failures, arithmetic rounding errors and specification-implementation differences, which were addressed in versions 3.1.3 and 3.2.0. Formal verification can test defined properties in a mathematical model and compare equivalent inputs with production code, but it cannot eliminate borrower default risk, underwriting risk or failures in external operations. Validators will ultimately decide whether LendingProtocolV1_1 becomes active.