​
Use Case

In DeFi lending protocols, positions can be liquidated when they become unhealthy due to market movements or other factors. The health factor is a critical security parameter that determines when a position can be liquidated. An incorrect health factor calculation or validation could lead to:

  • Unauthorized liquidations of healthy positions
  • Loss of user funds through forced liquidations
  • Protocol insolvency if positions can’t be liquidated when needed
  • Market manipulation through targeted liquidations

This assertion is particularly important for:

  • Preventing liquidations of positions that are still healthy
  • Ensuring liquidations only occur when necessary for protocol solvency
  • Protecting users from unfair liquidations
  • Maintaining protocol stability by enforcing proper liquidation thresholds

​
Applicable Protocols

  • Lending protocols (e.g., Aave, Compound, Morpho) where positions can be liquidated
  • Margin trading platforms that require position health monitoring
  • Perpetual futures protocols with liquidation mechanisms
  • Any DeFi protocol that uses health factors to determine position solvency

These protocols need this assertion because:

  • Lending protocols rely on liquidations to maintain solvency
  • Margin trading platforms need precise health factor calculations
  • Perpetual futures protocols use liquidations for risk management
  • Incorrect liquidation logic could lead to significant protocol losses

​
Explanation

The assertion implements a multi-layered approach to verify liquidation health factors:

  1. Pre-liquidation Check:

    • Uses forkPreState() to capture the health factor before liquidation
    • Verifies the position is actually unhealthy (below liquidation threshold)
    • Prevents liquidations of healthy positions

  2. Post-liquidation Validation:

    • Uses forkPostState() to verify the health factor after liquidation
    • Ensures the health factor improves after liquidation
    • Confirms the position meets minimum health requirements

  3. Parameter Validation:

    • Uses getCallInputs() to monitor liquidation function calls
    • Validates that seized assets and repaid shares are non-zero
    • Enforces a maximum liquidation amount to prevent protocol destabilization
    • Ensures liquidation parameters are within safe bounds

The assertion uses the following cheatcodes:

  • forkPreState(): Captures the health factor before liquidation
  • forkPostState(): Verifies the health factor after liquidation
  • getCallInputs(): Monitors liquidation function calls
  • registerCallTrigger(): Triggers on liquidation function calls

This approach ensures that:

  1. Only unhealthy positions can be liquidated
  2. Liquidations improve the position’s health
  3. The protocol maintains proper risk management
  4. Liquidation amounts are within safe limits

For more information about cheatcodes, see the Cheatcodes Documentation.

​
Code Example

// SPDX-License-Identifier: MIT
pragma solidity 0.8.29;

import {Assertion} from "credible-std/Assertion.sol";
import {PhEvm} from "credible-std/PhEvm.sol";

// Using a generic lending protocol interface
interface ILendingProtocol {
    // MarketParams contains the market identifier
    // Using nested structs to match common lending protocol patterns
    struct MarketParams {
        Id id;
    }

    struct Id {
        uint256 marketId;
    }

    function liquidate(
        MarketParams memory marketParams,
        address borrower,
        uint256 seizedAssets,
        uint256 repaidShares,
        bytes memory data
    ) external returns (uint256, uint256);

    function isHealthy(MarketParams memory marketParams, address borrower) external view returns (bool);
    function healthFactor(MarketParams memory marketParams, address borrower) external view returns (uint256);
}

contract LiquidationHealthFactorAssertion is Assertion {
    ILendingProtocol public lendingProtocol;

    // Health factors are typically scaled by 1e18 for precision
    // This allows for fine-grained health factor calculations without floating point
    uint256 constant LIQUIDATION_THRESHOLD = 1e18; // 1.0
    uint256 constant MIN_HEALTH_FACTOR = 1.02e18; // 1.02 - small buffer above liquidation

    // Maximum amount that can be liquidated in a single transaction
    // This helps prevent large liquidations that could destabilize the protocol
    uint256 constant MAX_LIQUIDATION_AMOUNT = 1000e18; // Example value, adjust based on protocol

    constructor(address lendingProtocol_) {
        lendingProtocol = ILendingProtocol(lendingProtocol_);
    }

    function triggers() external view override {
        // Register trigger for liquidation function calls
        registerCallTrigger(this.assertHealthFactor.selector, lendingProtocol.liquidate.selector);
    }

    // Make sure that liquidation can't happen if the position is healthy
    // Check that the health factor is improved after liquidation
    function assertHealthFactor() external {
        // Get all liquidation calls in the transaction
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(lendingProtocol), lendingProtocol.liquidate.selector);

        for (uint256 i = 0; i < callInputs.length; i++) {
            address borrower;
            ILendingProtocol.MarketParams memory marketParams;
            uint256 seizedAssets;
            uint256 repaidShares;

            // Decode liquidation parameters
            (marketParams, borrower, seizedAssets, repaidShares,) =
                abi.decode(callInputs[i].input, (ILendingProtocol.MarketParams, address, uint256, uint256, bytes));

            // Validate liquidation amounts
            require(seizedAssets > 0, "Zero assets seized");
            require(repaidShares > 0, "Zero shares repaid");
            require(seizedAssets <= MAX_LIQUIDATION_AMOUNT, "Liquidation amount too large");

            // Check health factor before liquidation
            ph.forkPreState();
            uint256 preHealthFactor = lendingProtocol.healthFactor(marketParams, borrower);
            require(preHealthFactor <= LIQUIDATION_THRESHOLD, "Account not eligible for liquidation");

            // Check health factor after liquidation
            ph.forkPostState();
            uint256 postHealthFactor = lendingProtocol.healthFactor(marketParams, borrower);

            // Verify the liquidation actually improved the position's health
            require(postHealthFactor > preHealthFactor, "Health factor did not improve after liquidation");

            // Ensure the position is now in a safe state above the minimum required health factor
            // This prevents partial liquidations that leave positions in a dangerous state
            require(postHealthFactor >= MIN_HEALTH_FACTOR, "Position still unhealthy after liquidation");
        }
    }
}

Note: This code example is maintained in the Phylax Assertion Examples Repository. For the latest version and a test example, please refer to the repository.

​
Testing

To test this assertion:

  1. Deploy a test instance of the lending protocol
  2. Create positions with varying health factors
  3. Attempt liquidations on both healthy and unhealthy positions
  4. Verify the assertion correctly:
    • Prevents liquidations of healthy positions
    • Allows liquidations of unhealthy positions
    • Ensures health factor improvement after liquidation

​
Assertion Best Practices

  • Combine with other assertions like ERC20 Drain for comprehensive protection
  • Use appropriate health factor thresholds based on protocol risk parameters