  Lending pools are decentralized applications which allow mutually untrusted
users to lend and borrow crypto-assets. These applications feature complex,
highly parametric incentive mechanisms to equilibrate the loan market. This
complexity makes the behaviour of lending pools difficult to understand and to
predict: indeed, ineffective incentives and attacks could potentially lead to
emergent unwanted behaviours. Reasoning about lending pools is made even harder
by the lack of executable models of their behaviour: to precisely understand
how users interact with lending pools, eventually one has to inspect their
implementations, where the incentive mechanisms are intertwined with low-level
implementation details. Further, the variety of existing implementations makes
it difficult to distill the common aspects of lending pools. We systematize the
existing knowledge about lending pools, leveraging a new formal model of
interactions with users, which reflects the archetypal features of mainstream
implementations. This enables us to prove some general properties of lending
pools, such as the correct handling of funds, and to precisely describe
vulnerabilities and attacks. We also discuss the role of lending pools in the
broader context of decentralized finance.
