### Abstract

We construct an abstract ledger supporting the risk-free lending protocol. The risk-free lending protocol is a system for issuing and exchanging novel financial products we call risk-free loans. The system allows one party to lend money at 0% APY to another party in exchange for a good or service. On every update of the ledger, accounts have interest distributed to them. Holders of lent assets keep interest accrued by those assets. After distributing interest, the system returns a fixed fraction of each loan. These fixed fractions determine loan periods. Loans for longer periods have a smaller fixed fraction returned. Loans may be re-lent or used as collateral for other loans. We give a sufficient criterion to enforce that all accounts will forever be solvent. We give a protocol for maintaining this invariant when transferring or lending funds. We also show that this invariant holds after an update. Even though the system does not track counter-party obligations, we show that all credited and debited loans cancel, and the monetary supply grows at a specified interest rate.

### License

BSD License

### Topics

- Mathematics/Games and economics

### Related publications

- Doty, M. (2022). Risk-Free Lending. SSRN Electronic Journal. https://doi.org/10.2139/ssrn.4254003

### Session Risk_Free_Lending

- Risk_Free_Lending

## Cite

×

Risk_Free_Lending-AFP

    @article{Risk_Free_Lending-AFP,
      author  = {Matthew Doty},
      title   = {Risk-Free Lending},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Risk_Free_Lending.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 22, 2022 : Isabelle2021-1