Prove your protocol never loses funds
with invariants.

We’ll implement a small protocol with:

• Users deposit ETH as collateral
• Users borrow a stable ERC-20 against collateral
• An oracle provides ETH price
• Health factor enforces solvency
• Repay & withdraw flows

2.1 USDToken (mintable ERC-20)

Create src/USDToken.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "@openzeppelin/contracts/token/ERC20/ERC20.sol";

contract USDToken is ERC20 {
    address public minter;

    constructor() ERC20("USDToken", "USDT") {}

    function setMinter(address m) external {
        require(minter == address(0), "minter already set");
        minter = m;
    }

    modifier onlyMinter() {
        require(msg.sender == minter, "not minter");
        _;
    }

    function mint(address to, uint256 amt) external onlyMinter {
        _mint(to, amt);
    }

    function burn(address from, uint256 amt) external onlyMinter {
        _burn(from, amt);
    }
}

2.2 Price oracle (simplified)

Create src/Oracle.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract Oracle {
    // price in USD with 18 decimals
    uint256 public price = 2000e18;

    function setPrice(uint256 newPrice) external {
        price = newPrice;
    }
}

2.3 LendingPool core

Create src/LendingPool.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "./USDToken.sol";
import "./Oracle.sol";

contract LendingPool {
    USDToken public immutable usd;
    Oracle  public immutable oracle;

    // user collateral in wei
    mapping(address => uint256) public collateral;
    // user debt in USDT (18d)
    mapping(address => uint256) public debt;

    // constants
    uint256 public constant LTV = 75e16;  // 0.75 * 1e18
    uint256 public constant LIQ_THRESHOLD = 80e16; // 0.8 * 1e18

    constructor(USDToken _usd, Oracle _oracle) {
        usd = _usd;
        oracle = _oracle;
    }

    // --- Views ---

    function ethPrice() public view returns (uint256) {
        return oracle.price(); // USD per ETH, 18d
    }

    function collateralValueUsd(address user) public view returns (uint256) {
        return collateral[user] * ethPrice() / 1e18;
    }

    function maxBorrowUsd(address user) public view returns (uint256) {
        return collateralValueUsd(user) * LTV / 1e18;
    }

    function healthFactor(address user) public view returns (uint256) {
        uint256 d = debt[user];
        if (d == 0) return type(uint256).max;
        // collateral * threshold / debt
        return collateralValueUsd(user) * LIQ_THRESHOLD / d;
    }

    // --- Actions ---

    function deposit() external payable {
        collateral[msg.sender] += msg.value;
    }

    function withdraw(uint256 amountWei) external {
        require(collateral[msg.sender] >= amountWei, "not enough collateral");
        collateral[msg.sender] -= amountWei;
        require(healthFactor(msg.sender) >= 1e18, "HF<1 after withdraw");

        (bool ok,) = msg.sender.call{value: amountWei}("");
        require(ok, "eth transfer failed");
    }

    function borrow(uint256 amountUsd) external {
        require(amountUsd > 0, "zero borrow");
        uint256 maxB = maxBorrowUsd(msg.sender);
        require(debt[msg.sender] + amountUsd <= maxB, "exceeds LTV");

        debt[msg.sender] += amountUsd;
        usd.mint(msg.sender, amountUsd);
        require(healthFactor(msg.sender) >= 1e18, "HF<1 after borrow");
    }

    function repay(uint256 amountUsd) external {
        require(amountUsd > 0, "zero repay");
        uint256 d = debt[msg.sender];
        uint256 pay = amountUsd > d ? d : amountUsd;

        debt[msg.sender] -= pay;
        usd.burn(msg.sender, pay);
    }
}

We start with a few deterministic tests just to ensure the model works.

Create test/LendingPool.unit.t.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "forge-std/Test.sol";
import "../src/USDToken.sol";
import "../src/Oracle.sol";
import "../src/LendingPool.sol";

contract LendingPoolUnitTest is Test {
    USDToken usd;
    Oracle oracle;
    LendingPool pool;

    address alice = address(0xA11CE);
    address bob   = address(0xB0B);

    function setUp() public {
        usd = new USDToken();
        oracle = new Oracle();
        pool = new LendingPool(usd, oracle);
        usd.setMinter(address(pool));

        vm.deal(alice, 100 ether);
        vm.deal(bob, 100 ether);
    }

    function test_depositAndBorrow() public {
        vm.startPrank(alice);
        pool.deposit{value: 10 ether}();

        // ETH price 2000 => 10 ETH == 20k USD
        // LTV 75% => max borrow 15k
        pool.borrow(15_000e18);

        assertEq(pool.debt(alice), 15_000e18);
        assertEq(usd.balanceOf(alice), 15_000e18);
        assertTrue(pool.healthFactor(alice) >= 1e18);
        vm.stopPrank();
    }

    function test_repayAndWithdraw() public {
        vm.startPrank(alice);
        pool.deposit{value: 10 ether}();
        pool.borrow(10_000e18);

        pool.repay(4_000e18);
        assertEq(pool.debt(alice), 6_000e18);

        pool.withdraw(2 ether);
        assertEq(pool.collateral(alice), 8 ether);

        vm.stopPrank();
    }

    function test_priceDropCanMakeHFBelow1() public {
        vm.startPrank(alice);
        pool.deposit{value: 10 ether}();
        pool.borrow(14_000e18);
        vm.stopPrank();

        // ETH price drops to 1200
        oracle.setPrice(1200e18);

        // HF should dip below 1
        assertTrue(pool.healthFactor(alice) < 1e18);
    }
}

Run:

forge test --match-test test_ -vv

Before coding, write down the properties you want to guarantee. A good invariant is:

• Simple to state
• Hard to break accidentally
• Meaningful for users / funds

Invariant #1 — protocol solvency

The pool should never “create” debt without enough collateral to justify it. In our model, solvency means:

sum(collateralValueUsd(users)) * LIQ_THRESHOLD
    >= sum(debt(users))

If this ever fails, the protocol is underwater and someone can withdraw more than is safe.

Invariant #2 — no negative balances

User collateral and debt mappings should never underflow. Solidity 0.8 already reverts on underflow, but we still want to assert:

collateral[user] >= 0
debt[user] >= 0

Invariant #3 — minted supply equals total debt

Since the pool is the only minter/burner of USDToken in this model, total supply should always match sum of user debts:

usd.totalSupply() == sum(debt(users))

Invariant #4 — health factor can only be < 1 due to price moves

Users should not be able to make themselves unhealthy via actions (borrow/withdraw enforce HF ≥ 1). So:

after any user action:
  healthFactor(user) >= 1e18
unless oracle price changed externally

We’ll encode this by modeling oracle moves as a separate handler action and tracking whether price changed in the current sequence.

Foundry invariants work like this:

1. You create a Handler contract with actions.
2. Foundry randomly calls these actions in sequences.
3. After each sequence, it checks invariant functions.

Create test/Handler.t.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "forge-std/Test.sol";
import "../src/USDToken.sol";
import "../src/Oracle.sol";
import "../src/LendingPool.sol";

contract Handler is Test {
    LendingPool public pool;
    USDToken public usd;
    Oracle public oracle;

    address[] public users;
    bool public priceMoved;

    constructor(LendingPool _pool, USDToken _usd, Oracle _oracle, address[] memory _users) {
        pool = _pool;
        usd = _usd;
        oracle = _oracle;
        users = _users;
    }

    // Pick a user by fuzzed index
    function _user(uint256 seed) internal view returns (address) {
        return users[seed % users.length];
    }

    // --- Actions ---

    function act_deposit(uint256 userSeed, uint256 amountWei) public {
        address u = _user(userSeed);

        // bound amount to realistic range
        uint256 amt = bound(amountWei, 0.1 ether, 20 ether);

        vm.deal(u, u.balance + amt);
        vm.prank(u);
        pool.deposit{value: amt}();
    }

    function act_withdraw(uint256 userSeed, uint256 amountWei) public {
        address u = _user(userSeed);

        uint256 col = pool.collateral(u);
        if (col == 0) return;

        uint256 amt = bound(amountWei, 0, col);

        vm.prank(u);
        // withdraw may revert if HF<1, that's ok
        try pool.withdraw(amt) {} catch {}
    }

    function act_borrow(uint256 userSeed, uint256 amountUsd) public {
        address u = _user(userSeed);

        uint256 maxB = pool.maxBorrowUsd(u);
        uint256 d = pool.debt(u);
        if (maxB <= d) return;

        uint256 room = maxB - d;
        uint256 amt = bound(amountUsd, 1e18, room);

        vm.prank(u);
        try pool.borrow(amt) {} catch {}
    }

    function act_repay(uint256 userSeed, uint256 amountUsd) public {
        address u = _user(userSeed);

        uint256 d = pool.debt(u);
        if (d == 0) return;

        uint256 amt = bound(amountUsd, 1e18, d);

        // ensure user has enough USD to repay
        vm.startPrank(u);
        if (usd.balanceOf(u) < amt) {
            // minting to user should only happen via borrow,
            // but for testing we allow top-up to explore repay paths
            usd.mint(u, amt - usd.balanceOf(u));
        }

        try pool.repay(amt) {} catch {}
        vm.stopPrank();
    }

    function act_movePrice(uint256 newPrice) public {
        // allow oracle moves in a broad range
        uint256 p = bound(newPrice, 300e18, 5000e18);
        oracle.setPrice(p);
        priceMoved = true;
    }

    function resetPriceMoved() public {
        priceMoved = false;
    }
}

Now we create Foundry’s invariant harness. This is the contract where invariants live.

Create test/LendingPool.invariant.t.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "forge-std/Test.sol";
import "forge-std/StdInvariant.sol";
import "../src/USDToken.sol";
import "../src/Oracle.sol";
import "../src/LendingPool.sol";
import "./Handler.t.sol";

contract LendingPoolInvariantTest is StdInvariant, Test {
    USDToken usd;
    Oracle oracle;
    LendingPool pool;
    Handler handler;

    address[] users;

    function setUp() public {
        usd = new USDToken();
        oracle = new Oracle();
        pool = new LendingPool(usd, oracle);
        usd.setMinter(address(pool));

        // create a small user set
        users.push(address(0xA11CE));
        users.push(address(0xB0B));
        users.push(address(0xCAFE));
        users.push(address(0xD00D));

        for (uint256 i = 0; i < users.length; i++) {
            vm.deal(users[i], 200 ether);
        }

        handler = new Handler(pool, usd, oracle, users);

        // Tell Foundry to fuzz handler functions
        targetContract(address(handler));

        // optional: reduce or bias specific selectors
        bytes4;
        selectors[0] = Handler.act_deposit.selector;
        selectors[1] = Handler.act_withdraw.selector;
        selectors[2] = Handler.act_borrow.selector;
        selectors[3] = Handler.act_repay.selector;
        selectors[4] = Handler.act_movePrice.selector;

        targetSelector(FuzzSelector({
            addr: address(handler),
            selectors: selectors
        }));
    }

    // --- helper to sum debt & collateral ---

    function _sumDebt() internal view returns (uint256 total) {
        for (uint256 i = 0; i < users.length; i++) {
            total += pool.debt(users[i]);
        }
    }

    function _sumCollUsd() internal view returns (uint256 total) {
        for (uint256 i = 0; i < users.length; i++) {
            total += pool.collateralValueUsd(users[i]);
        }
    }

    // --- Invariants ---

    // Invariant #1: Solvency
    function invariant_protocolSolvent() public {
        uint256 totalDebt = _sumDebt();
        uint256 totalColUsd = _sumCollUsd();

        uint256 thresholdCol = totalColUsd * pool.LIQ_THRESHOLD() / 1e18;

        assertGe(thresholdCol, totalDebt, "protocol insolvent");
    }

    // Invariant #2: totalSupply == sum(debt)
    function invariant_supplyEqualsDebt() public {
        assertEq(usd.totalSupply(), _sumDebt(), "supply != debt");
    }

    // Invariant #3: no action can make HF < 1
    function invariant_actionsDontBreakHF() public {
        if (handler.priceMoved()) return;

        for (uint256 i = 0; i < users.length; i++) {
            assertGe(
                pool.healthFactor(users[i]),
                1e18,
                "HF<1 without price move"
            );
        }
    }

    // reset flag between sequences
    function afterInvariant() public {
        handler.resetPriceMoved();
    }
}

You now have a full invariant system: Foundry will call handler actions randomly, then validate invariants.

Run invariants:

forge test --match-test invariant_ -vv

Let’s create a bug by commenting out the HF check in withdraw:

// require(healthFactor(msg.sender) >= 1e18, "HF<1 after withdraw");

Run invariants again.

You should see a failure similar to:

Failing tests:
invariant_protocolSolvent()
  error: protocol insolvent
  counterexample:
    act_deposit(u=alice, 10 ETH)
    act_borrow(u=alice, 15000 USD)
    act_withdraw(u=alice, 9 ETH)

7.1 Read the counterexample

The fuzzer found a sequence where Alice withdraws too much collateral, leaving total debt above solvency threshold.

7.2 Re-run with the replay

Foundry provides a replay call in logs. Use:

forge test --match-test invariant_protocolSolvent --replay-path <path> -vvvv

With high verbosity you’ll see the full trace and can insert logs.

Re-enable the HF check to fix the protocol.

Tip A — prefer small user sets

Invariants scale poorly with many accounts. Start with 3-8 users. Add more only if needed.

Tip B — handlers should not revert often

If most fuzz calls revert, you lose exploration. Use bounds, early returns, and try/catch to keep actions “soft”.

Tip C — track ghost state for totals

If your protocol tracks internal totals (like reserves), store parallel “ghost” totals in Handler and assert equality. That catches accounting drift fast.

Tip D — separate “environment moves”

Oracles, time, or L2 fees are environment actions. Keep them as separate selectors so invariants can allow changes only when the environment moved.