Property Design Patterns for DeFi Lending Protocols

Writing invariant properties is an art. Write them too broadly and they never fail. Write them too narrowly and they miss real bugs. Here are six battle-tested property design patterns for DeFi lending protocols — the ones I keep coming back to across every lending engagement.

Each pattern includes the rationale, a Solidity implementation compatible with the Chimera framework, and notes on common pitfalls.

Pattern 1: The Solvency Invariant

What it checks: The protocol always holds enough assets to cover all obligations.

This is the single most important property for any lending protocol. If this breaks, the protocol is insolvent.

function invariant_solvency() public returns (bool) {
    uint256 totalDeposited = lendingPool.totalDepositAssets();
    uint256 totalBorrowed = lendingPool.totalBorrowAssets();
    uint256 protocolBalance = underlying.balanceOf(address(lendingPool));

    // Cash on hand + outstanding borrows must cover all deposits
    return protocolBalance + totalBorrowed >= totalDeposited;
}

Pitfall: Make sure to account for accrued interest on both sides. If interest accrues to deposits but has not been added to totalBorrowed, this can produce false positives.

Pattern 2: Utilization Rate Bounds

What it checks: The utilization rate stays within protocol-defined bounds at all times.

function invariant_utilizationBounds() public returns (bool) {
    uint256 totalDeposited = lendingPool.totalDepositAssets();
    if (totalDeposited == 0) return true;

    uint256 totalBorrowed = lendingPool.totalBorrowAssets();
    uint256 utilization = (totalBorrowed * 1e18) / totalDeposited;

    // Utilization cannot exceed 100%
    // (borrowing more than deposited should be impossible)
    return utilization <= 1e18;
}

Why it matters: If utilization exceeds 100%, the protocol has somehow allowed borrowing more than what was deposited. This would indicate a critical accounting flaw.

Extended version: Some protocols have target utilization ranges enforced by interest rate curves. You can tighten this property to verify the interest rate model enforces those bounds correctly.

Pattern 3: Interest Rate Monotonicity

What it checks: The borrow rate increases (or stays constant) as utilization increases.

function property_interestRateMonotonicity(
    uint256 utilA,
    uint256 utilB
) public returns (bool) {
    utilA = clamp(utilA, 0, 1e18);
    utilB = clamp(utilB, 0, 1e18);

    if (utilA >= utilB) return true;

    uint256 rateA = interestModel.getBorrowRate(utilA);
    uint256 rateB = interestModel.getBorrowRate(utilB);

    // Higher utilization must produce higher (or equal) borrow rate
    return rateB >= rateA;
}

Why it matters: A non-monotonic interest rate curve can create arbitrage opportunities. If rates decrease at high utilization, borrowers are incentivized to borrow more precisely when liquidity is scarce. This drains the pool.

Pattern 4: Liquidation Health Factor

What it checks: Every position that exists has not silently become liquidatable without the protocol noticing.

function invariant_noUnderwaterPositions() public returns (bool) {
    for (uint256 i = 0; i < actors.length; i++) {
        address user = actors[i];
        uint256 borrowed = lendingPool.borrowBalance(user);
        if (borrowed == 0) continue;

        uint256 collateralValue = lendingPool.getCollateralValue(user);
        uint256 minCollateral = (borrowed * lendingPool.liquidationThreshold())
            / 1e18;

        // If a position is underwater, it MUST be liquidatable
        if (collateralValue < minCollateral) {
            // Verify liquidation would succeed
            try lendingPool.liquidate(user, borrowed / 2) {
                // Liquidation succeeded — this is correct behavior
            } catch {
                // Underwater position that cannot be liquidated = critical bug
                return false;
            }
        }
    }
    return true;
}

Why it matters: A position that is underwater but cannot be liquidated is a ticking time bomb. Bad debt accumulates and eventually leads to insolvency. This property ensures the liquidation mechanism actually works when needed.

Pattern 5: Share Price Monotonicity

What it checks: The exchange rate between deposit shares and underlying assets never decreases (outside of legitimate loss events).

// Store the previous share price in a ghost variable
uint256 internal previousSharePrice;

function invariant_sharePriceMonotonicity() public returns (bool) {
    uint256 currentSharePrice = lendingPool.totalDepositAssets() * 1e18
        / lendingPool.totalDepositShares();

    // Share price should only increase (from interest accrual)
    bool result = currentSharePrice >= previousSharePrice;
    previousSharePrice = currentSharePrice;
    return result;
}

Why it matters: If the share price ever decreases without an explicit loss event (like a liquidation with bad debt), it means value is leaking from depositors. Common causes include incorrect interest accrual, rounding in the wrong direction, or reward distribution bugs.

Pitfall: Some protocols intentionally allow share price to decrease during socialized loss events. Account for this in your property by tracking whether a loss event occurred.

Pattern 6: Collateral Accounting Consistency

What it checks: The sum of all individual collateral balances equals the total collateral tracked by the protocol.

function invariant_collateralAccounting() public returns (bool) {
    uint256 sumOfBalances = 0;
    for (uint256 i = 0; i < actors.length; i++) {
        sumOfBalances += lendingPool.collateralBalance(actors[i]);
    }

    // Sum of individual balances must equal protocol total
    return sumOfBalances == lendingPool.totalCollateral();
}

Why it matters: Discrepancies between individual and aggregate accounting are the root cause of many DeFi exploits. If the sum of individual balances exceeds the total, the protocol will run out of collateral. If it is less, funds are locked.

Structuring Properties in Chimera

When using the Chimera framework, organize your properties in a dedicated Properties.sol contract that inherits from your BeforeAfter helper:

// Properties.sol
import {BeforeAfter} from "./BeforeAfter.sol";

contract Properties is BeforeAfter {
    function invariant_solvency() public returns (bool) { /* ... */ }
    function invariant_utilizationBounds() public returns (bool) { /* ... */ }
    // ... more properties
}

The BeforeAfter pattern lets you capture state snapshots before and after each call, making it easy to write transition properties like share price monotonicity. For a full guide on Chimera's architecture, see Invariant Testing with Chimera.

Combining Properties for Maximum Coverage

These six patterns cover the core safety properties of any lending protocol. In practice, you will want to combine them and add protocol-specific properties. The key insight is that simple properties catch the most bugs. Start with solvency and accounting consistency before moving to more exotic properties.

In a typical lending engagement, we end up with 15-30 properties, and these six patterns form the foundation every time. The rest target protocol-specific logic: governance mechanisms, oracle integrations, fee calculations, and cross-market interactions.

Ready to build a comprehensive invariant test suite for your lending protocol? Request an audit with Recon and get battle-tested properties tailored to your specific architecture.