Paper: A Theory of Lending Protocols in DeFi Authors: Massimo Bartoletti, Enrico Lipparini Date: June 18, 2025 Estimated Reading Time: 30 minutes
This paper introduces a formal operational model for decentralized lending protocols like Aave and Compound. It models these systems as state machines to analyze their structural properties, user incentives, and vulnerabilities. The model includes wallet and lending pool states, collateral and debt tracking, and price oracles. The paper identifies invariants like net worth conservation and studies economic effects of actions like borrowing, liquidation, and interest accrual. It also evaluates strategies for rational and adversarial users, showing how they can front-run events or manipulate system parameters like prices or utilization. The authors provide formal proofs for strategic behavior and various attack scenarios.
Core Insights:
- Formal Model of Lending Protocols: The paper presents lending protocols as state machines, separating wallet states, lending pools, and price oracles. This abstraction allows rigorous analysis of user behavior and protocol mechanics under different economic actions.
- Invariant Preservation: The authors prove structural properties such as the preservation of total user net worth under most transactions (excluding price updates), and monotonic exchange rates which only increase due to interest accrual.
- Impact of Individual Transactions: Each transaction type-deposit, borrow, repay, redeem, interest accrual, liquidation-has quantified effects on net worth and collateralization. Liquidation is the only user-triggered transaction that affects net worth directly.
- Rational and Strategic Behavior: Rational users can front-run liquidations or price updates for gain. However, in most settings with dynamic interest rates, there’s no consistent advantage from preemptive actions without detailed context-specific information.
- Formalized Attack Scenarios: The model reveals how adversaries can profit via price and utilization manipulation, borrowing excess assets or influencing interest rate shifts. These attack vectors are proven under specific conditions.
The authors’ operational model provides a rigorous foundation for analyzing decentralized lending protocols’ economic mechanics. By framing interactions as state transitions, the paper offers mathematical clarity into how assets, debts, and user strategies evolve over time. The primary structural invariant that net worth is preserved barring price changes grounds the analysis and demonstrates the protocol’s internal balance. Importantly, the distinction between real net worth and disposable wealth shows that users’ actual financial freedom can differ significantly from their accounting value, especially during liquidity shortages or attacks.
The paper excels in detailing the effect of every transaction type. Deposits and repayments increase a user’s health factor (a measure of safety from liquidation), while borrowing and redeeming do the opposite. The health factor metric, derived from collateralization ratios, determines whether a user’s assets are safe or subject to liquidation. Liquidations reward liquidators with a portion of the collateral, providing financial incentive but also creating gameable vulnerabilities. A key insight is that liquidators only act when they can profit, meaning users must maintain health factors above the critical threshold to avoid loss.
From a demand perspective, the protocol ensures borrowers are always incentivized to stay over-collateralized. Credit tokens appreciate through interest accruals, pushing lenders to supply liquidity. However, dynamic interest rates tied to utilization create new strategic possibilities. Users may game the timing of interest accruals or price changes to increase their position value. Yet, the analysis finds that in most cases, only liquidation and price changes materially affect net worth, unless the user has foreknowledge or the system uses fixed rates.
The formal treatment of attacks is especially insightful. For example, in a price manipulation attack, an adversary temporarily changes token prices to borrow more or trigger liquidations. Similarly, utilization manipulation (by sudden deposits or borrows) alters interest rates in the attacker’s favor. These scenarios are not hypothetical; the authors prove the exact conditions under which each attack is economically viable, highlighting the need for robust oracle design and usage limits.
The model’s abstraction omits real-world features like slippage or gas costs, but this simplification strengthens its clarity. However, it raises questions: Can similar invariant preservation hold when such costs are added? How would slippage affect front-running profitability? The paper also assumes deterministic actions and continuous token values, diverging from on-chain implementations that use discrete token balances. While this allows smooth mathematical treatment, exploring edge cases in discrete systems could reveal different vulnerabilities.
Overall, the paper is a cornerstone for DeFi protocol designers seeking to understand the underlying economics of lending mechanisms. It offers proof-based insight into not just what can go wrong, but under which circumstances. Future work might extend the model to multi-token systems with interconnected lending and borrowing positions, or explore incentive-compatible design to mitigate the attacks demonstrated.
