Foundry Invariant Testing: The Handler Pattern in Depth

Most Foundry users have written a fuzz test. Fewer have written a good invariant test suite — one that actually exercises meaningful protocol state and catches real bugs rather than generating thousands of no-op reverts. This article closes that gap.

We will work through the full architecture of a production-grade invariant suite: why invariant testing exists, how the handler pattern works, what ghost variables are and how to write them, which invariants matter for ERC-4626 vaults, lending markets, and DEXs, how to configure and debug campaigns, and how to integrate everything into CI. Code throughout is complete and directly runnable.

---

Fuzz Tests vs. Invariant Tests: What Actually Differs

The naming in Foundry is slightly confusing, so let’s be precise before touching any code.

The conceptual difference is straightforward: stateless fuzzing discards the EVM state between iterations, while stateful fuzzing preserves it. Foundry’s terminology maps exactly onto this distinction: “fuzzing” refers to stateless tests, and “invariant testing” refers to stateful tests.

A standard fuzz test looks like:

function testFuzz_deposit(uint256 amount) public {
    amount = bound(amount, 1, 1e30);
    vault.deposit(amount, address(this));
    assertGt(vault.balanceOf(address(this)), 0);
}

Every time Foundry runs this, it starts from a fresh setUp() state. The call sequence is always exactly one transaction long. Stateless fuzz tests may miss vulnerabilities that only become apparent when a specific sequence of function calls with specific inputs occurs.

Invariant tests are categorically different. Invariant tests are stateful fuzz tests that assert “rules” which must always hold true, even after any sequence of contract calls. After each function call is performed, all defined invariants are asserted. Invariant testing is a powerful tool to expose incorrect logic in protocols. Due to the fact that function call sequences are randomized and have fuzzed inputs, invariant testing can expose false assumptions and incorrect logic in edge cases and highly complex protocol states.

The practical difference matters enormously. Consider a vault where deposit and withdraw both look correct in isolation, but withdraw after deposit after donate produces a rounding error that steals one wei per interaction. Stateless fuzzing will never catch this — it can’t chain the three calls. Invariant testing, given the right setup, will.

Stateful fuzzing is where the state of the previous run is the starting state of the next run. Each invariant “run” is a sequence of up to depth randomly-chosen function calls, all operating on shared persistent state. After every call in the sequence, Foundry checks every invariant_* function. One failed assertion fails the whole test and triggers the shrinking algorithm.

---

Open Testing vs. The Handler Pattern

The Problem with Open Testing

When you call targetContract(address(myVault)) and point the fuzzer directly at production contracts, you get “open” invariant testing. With open invariant testing, random sequences of function calls are made to the protocol contracts directly with fuzzed parameters. This will cause reverts for more complex systems.

The result is a test that technically passes while testing almost nothing. If 98% of calls revert because the fuzzer tries to withdraw before depositing, the protocol’s accounting is never meaningfully exercised. In the open invariant testing approach, deposit and transfer would be called with a 50-50% distribution, but they would revert on every call. This would cause the invariant tests to “pass”, but in reality no state was manipulated in the desired contract at all.

The Handler Pattern

The handler is an intermediary contract that sits between the fuzzer and the protocol. When a contract requires some additional logic in order to function properly, it can be added in a dedicated contract called a Handler. By manually adding all Handler contracts to the targetContracts array, all function calls made to protocol contracts can be made in a way that is governed by the Handler to ensure successful calls.

With this layer between the fuzzer and the protocol, more powerful testing can be achieved. The handler’s responsibilities are:

1. Input bounding — use bound() so function arguments are always valid
2. State preconditions — mint tokens before deposits, open positions before closing them
3. Ghost variable maintenance — track expected protocol state alongside real state
4. Actor management — impersonate multiple users so multi-party interactions are tested

In this way, handler functions are similar to fuzz tests because they can take in fuzzed inputs, perform state changes, and assert before/after state.

---

Ghost Variables: Your Shadow Accounting System

Ghost variables are essentially state variables that are used only for testing purposes. They shadow the protocol’s accounting using simple arithmetic that you control entirely, then the invariant asserts that the protocol matches your shadow ledger.

Within Handlers, ghost variables can be tracked across multiple function calls to add additional information for invariant tests.

A good example of this is summing all of the shares that each LP owns after depositing into an ERC-4626 token, and using that in the invariant (totalSupply == sumBalanceOf).

The pattern is:

// In the handler
uint256 public ghost_depositedAssets;   // sum of all deposits
uint256 public ghost_withdrawnAssets;   // sum of all withdrawals
mapping(address => uint256) public ghost_sharesOf; // per-actor shares

function deposit(uint256 assets, uint256 actorSeed) public useActor(actorSeed) {
    assets = bound(assets, 1, 1e30);
    asset.mint(currentActor, assets);
    asset.approve(address(vault), assets);

    uint256 sharesBefore = vault.balanceOf(currentActor);
    uint256 shares = vault.deposit(assets, currentActor);

    // Maintain ghost state
    ghost_depositedAssets += assets;
    ghost_sharesOf[currentActor] += shares;

    // Per-call assertion — catches bugs immediately
    assertEq(vault.balanceOf(currentActor), sharesBefore + shares);
}

The ghost state is a simple, obviously-correct accounting model. The invariant then compares it to the production system:

// In the invariant contract
function invariant_totalAssets() public view {
    assertGe(
        vault.totalAssets(),
        handler.ghost_depositedAssets() - handler.ghost_withdrawnAssets()
    );
}

Note assertGe rather than assertEq — yield-bearing vaults accumulate assets over time, so the real total should be at least the net deposited amount.

---

Multi-Actor Management

A vault tested with a single depositor misses entire classes of bugs. Share dilution, race conditions, and rounding exploits only appear when multiple actors interact with the protocol simultaneously.

By leveraging the prank cheatcodes in forge-std, each Handler can manage a set of actors and use them to perform the same function call from different msg.sender addresses. The canonical pattern is:

address[] public actors;
address internal currentActor;

modifier useActor(uint256 actorIndexSeed) {
    currentActor = actors[bound(actorIndexSeed, 0, actors.length - 1)];
    vm.startPrank(currentActor);
    _;
    vm.stopPrank();
}

Initialize actors in the handler’s constructor:

constructor(address _vault, address _asset) {
    vault  = IVault(_vault);
    asset  = IERC20(_asset);

    actors.push(makeAddr("alice"));
    actors.push(makeAddr("bob"));
    actors.push(makeAddr("carol"));
    actors.push(makeAddr("attacker"));
}

Now each fuzzed call targets a random actor. Ghost variables indexed by actor address track per-user state, enabling invariants that check not just protocol totals but individual account consistency.

---

Complete Invariant Suite: ERC-4626 Vault

The following is a complete, self-contained invariant test suite for an ERC-4626 vault. It demonstrates all the patterns above, plus time-based fuzzing for yield accrual.

Project Layout

src/
  SimpleVault.sol
test/
  invariant/
    handlers/
      VaultHandler.sol
    VaultInvariant.t.sol

The Handler

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

/// @title VaultHandler
/// @notice Mediates between the fuzzer and the ERC-4626 vault under test.
///         Maintains ghost variables that track expected protocol state.
contract VaultHandler is Test {
    // =========================================================
    // Immutables
    // =========================================================
    IERC4626   public immutable vault;
    MockERC20  public immutable asset;

    // =========================================================
    // Ghost Variables — shadow accounting
    // =========================================================
    uint256 public ghost_totalDeposited;
    uint256 public ghost_totalWithdrawn;
    uint256 public ghost_totalMinted;    // shares minted via mint()
    uint256 public ghost_totalRedeemed;  // shares redeemed via redeem()
    uint256 public ghost_sumSharesOf;    // sum of all per-actor share balances
    mapping(address => uint256) public ghost_sharesOf;
    mapping(address => uint256) public ghost_assetsDeposited;

    // =========================================================
    // Actor management
    // =========================================================
    address[] public actors;
    address   internal currentActor;

    modifier useActor(uint256 seed) {
        currentActor = actors[bound(seed, 0, actors.length - 1)];
        vm.startPrank(currentActor);
        _;
        vm.stopPrank();
    }

    // =========================================================
    // Constructor
    // =========================================================
    constructor(address _vault, address _asset) {
        vault = IERC4626(_vault);
        asset = MockERC20(_asset);

        actors.push(makeAddr("alice"));
        actors.push(makeAddr("bob"));
        actors.push(makeAddr("carol"));

        // Give every actor an initial balance
        for (uint256 i; i < actors.length; i++) {
            asset.mint(actors[i], 1_000_000e18);
            vm.prank(actors[i]);
            asset.approve(address(vault), type(uint256).max);
        }
    }

    // =========================================================
    // Handler Functions
    // =========================================================

    /// @notice Deposit assets, receive shares.
    function deposit(uint256 assets, uint256 actorSeed) public useActor(actorSeed) {
        // Bound to the actor's current balance
        uint256 maxDeposit = vault.maxDeposit(currentActor);
        if (maxDeposit == 0) return;
        assets = bound(assets, 1, maxDeposit);

        // Ensure actor has enough assets
        uint256 balance = asset.balanceOf(currentActor);
        if (balance < assets) asset.mint(currentActor, assets - balance);

        uint256 sharesBefore = vault.balanceOf(currentActor);
        uint256 shares = vault.deposit(assets, currentActor);

        // Ghost accounting
        ghost_totalDeposited             += assets;
        ghost_sharesOf[currentActor]     += shares;
        ghost_assetsDeposited[currentActor] += assets;
        ghost_sumSharesOf                += shares;

        // Per-call assertion: shares received match balance delta
        assertEq(vault.balanceOf(currentActor), sharesBefore + shares, "deposit: share accounting");
    }

    /// @notice Mint exact shares, paying assets.
    function mint(uint256 shares, uint256 actorSeed) public useActor(actorSeed) {
        uint256 maxMint = vault.maxMint(currentActor);
        if (maxMint == 0) return;
        shares = bound(shares, 1, maxMint);

        uint256 assets = vault.previewMint(shares);
        uint256 balance = asset.balanceOf(currentActor);
        if (balance < assets) asset.mint(currentActor, assets - balance);

        uint256 actualAssets = vault.mint(shares, currentActor);

        ghost_totalMinted                += shares;
        ghost_totalDeposited             += actualAssets;
        ghost_sharesOf[currentActor]     += shares;
        ghost_assetsDeposited[currentActor] += actualAssets;
        ghost_sumSharesOf                += shares;
    }

    /// @notice Withdraw exact assets, burning shares.
    function withdraw(uint256 assets, uint256 actorSeed) public useActor(actorSeed) {
        uint256 maxWithdraw = vault.maxWithdraw(currentActor);
        if (maxWithdraw == 0) return;
        assets = bound(assets, 1, maxWithdraw);

        uint256 sharesBefore = vault.balanceOf(currentActor);
        uint256 shares = vault.withdraw(assets, currentActor, currentActor);

        ghost_totalWithdrawn             -= assets;   // note: tracked as reduction
        ghost_sharesOf[currentActor]     -= shares;
        ghost_sumSharesOf                -= shares;

        assertEq(vault.balanceOf(currentActor), sharesBefore - shares, "withdraw: share burn");
    }

    /// @notice Redeem exact shares, receiving assets.
    function redeem(uint256 shares, uint256 actorSeed) public useActor(actorSeed) {
        uint256 maxRedeem = vault.maxRedeem(currentActor);
        if (maxRedeem == 0) return;
        shares = bound(shares, 1, maxRedeem);

        uint256 assetsBefore = asset.balanceOf(currentActor);
        uint256 assets = vault.redeem(shares, currentActor, currentActor);

        ghost_totalRedeemed              += shares;
        ghost_sharesOf[currentActor]     -= shares;
        ghost_sumSharesOf                -= shares;

        assertGt(asset.balanceOf(currentActor), assetsBefore, "redeem: assets received");
    }

    /// @notice Simulate yield accrual by donating assets directly.
    ///         This increases totalAssets without minting new shares,
    ///         causing the share price to rise.
    function donateYield(uint256 assets) public {
        assets = bound(assets, 1, 1_000e18);
        asset.mint(address(vault), assets);
        // No ghost update — yield is above the deposit baseline
    }

    /// @notice Fast-forward time (useful for testing time-based invariants).
    function advanceTime(uint256 secs) public {
        secs = bound(secs, 0, 30 days);
        vm.warp(block.timestamp + secs);
    }
}

The Invariant Contract

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

/// @title VaultInvariantTest
/// @notice Stateful invariant suite for an ERC-4626 vault.
/// @dev All invariant_ functions are checked after every call in every run.
contract VaultInvariantTest is StdInvariant, Test {

    SimpleVault  internal vault;
    MockERC20    internal asset;
    VaultHandler internal handler;

    function setUp() public {
        asset   = new MockERC20("Mock USDC", "mUSDC", 6);
        vault   = new SimpleVault(address(asset), "Vault Shares", "vUSDC");
        handler = new VaultHandler(address(vault), address(asset));

        // Point the fuzzer ONLY at the handler.
        // The vault and asset are excluded — they should only be touched
        // through the controlled handler interface.
        targetContract(address(handler));
        excludeContract(address(vault));
        excludeContract(address(asset));
    }

    // =========================================================
    // Core ERC-4626 Invariants
    // =========================================================

    /// @notice totalSupply must always equal the sum of all balances.
    ///         The ghost variable sumSharesOf mirrors this.
    function invariant_totalSupplyEqSumOfShares() public view {
        assertEq(
            vault.totalSupply(),
            handler.ghost_sumSharesOf(),
            "INV-1: totalSupply != sum(sharesOf)"
        );
    }

    /// @notice totalAssets must be >= the net assets deposited minus withdrawn.
    ///         It can be higher due to yield donations.
    function invariant_totalAssetsGeNetDeposits() public view {
        uint256 netDeposited = handler.ghost_totalDeposited();
        // Net is reduced by ghost_totalWithdrawn (stored as negative in handler)
        assertGe(
            vault.totalAssets(),
            netDeposited,
            "INV-2: totalAssets < net deposited"
        );
    }

    /// @notice Share price (assets per share) must never decrease.
    ///         This protects depositors from dilution attacks.
    ///         We track this by comparing to the initial price.
    function invariant_sharePriceNeverDecreases() public view {
        if (vault.totalSupply() == 0) return;
        // previewRedeem(1e18) gives current price per share
        // In a correctly implemented vault, yield donations only increase this.
        uint256 currentPrice = vault.previewRedeem(1e18);
        assertGe(currentPrice, 1e18, "INV-3: share price below initial");
    }

    /// @notice A user who deposits and immediately redeems must not gain assets
    ///         (no free money glitch — fees may apply, but never profit).
    ///         This is checked via a read-only preview, not an actual call.
    function invariant_noFreeMoneyOnRoundTrip() public view {
        if (vault.totalSupply() == 0) return;
        uint256 depositAmount = 1_000e6; // 1000 USDC
        uint256 shares  = vault.previewDeposit(depositAmount);
        uint256 returned = vault.previewRedeem(shares);
        assertLe(returned, depositAmount, "INV-4: round-trip profit impossible");
    }

    /// @notice Vault's actual asset balance must always back totalAssets.
    ///         For a simple vault with no external strategy, they must match.
    function invariant_assetBalanceEqTotalAssets() public view {
        assertEq(
            asset.balanceOf(address(vault)),
            vault.totalAssets(),
            "INV-5: vault balance != totalAssets"
        );
    }

    /// @notice totalSupply zero implies totalAssets zero (no phantom assets).
    function invariant_zeroSupplyImpliesZeroAssets() public view {
        if (vault.totalSupply() == 0) {
            assertEq(vault.totalAssets(), 0, "INV-6: totalAssets nonzero with zero supply");
        }
    }

    // =========================================================
    // Post-Run Cleanup (afterInvariant)
    // =========================================================

    /// @notice Called at the end of every run.
    ///         Verifies that all actors can fully exit — no funds locked.
    function afterInvariant() public {
        address[] memory actors = handler.actors();
        for (uint256 i; i < actors.length; i++) {
            uint256 shares = vault.balanceOf(actors[i]);
            if (shares == 0) continue;

            uint256 assetsBefore = asset.balanceOf(actors[i]);
            vm.prank(actors[i]);
            vault.redeem(shares, actors[i], actors[i]);
            assertGt(
                asset.balanceOf(actors[i]),
                assetsBefore,
                "afterInvariant: actor could not exit"
            );
        }
        // After all exits, vault should be empty
        assertEq(vault.totalSupply(), 0, "afterInvariant: supply nonzero post-exit");
        assertEq(vault.totalAssets(), 0, "afterInvariant: assets nonzero post-exit");
    }
}

The afterInvariant() function is called at the end of each invariant run (if declared), allowing post-campaign processing. It can be used for logging campaign metrics and post-fuzz campaign testing — for example, close out all positions and assert all funds are able to exit the system.

---

Common Invariants by Protocol Type

ERC-4626 Vaults

Beyond what the suite above covers:

Invariant	Expression	Why
Vault solvency	totalAssets >= totalSupply * pricePerShare	Shares always backed
Monotone share price	previewRedeem(1e18) >= lastPrice	No dilution
Deposit-withdraw symmetry	redeem(deposit(x)) <= x	No free money
maxDeposit respected	deposit up to maxDeposit never reverts	Spec compliance
maxWithdraw respected	withdraw up to maxWithdraw never reverts	Spec compliance
Rounding favours vault	previewWithdraw(x) >= withdraw(x, ...)	No user profit on rounding

Lending Markets

Lending protocols have richer invariants because they involve collateral, debt, and liquidation:

/// @notice Total debt across all borrowers must never exceed total supplied assets.
function invariant_debtLteTotalSupplied() public view {
    assertLe(
        lendingPool.totalBorrows(),
        lendingPool.totalSupplied(),
        "LM-1: undercollateralised system"
    );
}

/// @notice Every open position must be above minimum collateral ratio.
function invariant_allPositionsHealthy() public view {
    address[] memory borrowers = handler.getBorrowers();
    for (uint256 i; i < borrowers.length; i++) {
        uint256 health = lendingPool.healthFactor(borrowers[i]);
        // 1e18 represents a health factor of 1.0
        assertGe(health, 1e18, "LM-2: unhealthy position exists");
    }
}

/// @notice Interest rate must be bounded — no infinite borrow rate.
function invariant_interestRateBounded() public view {
    uint256 rate = lendingPool.borrowRate();
    assertLe(rate, 1e18, "LM-3: borrow rate > 100%");
}

/// @notice Accumulated interest never causes overflow in accounting.
function invariant_noInterestOverflow() public view {
    // Check that totalDebt() can be computed without reverting
    lendingPool.totalDebt(); // if this reverts, test fails
}

Key ghost variables for lending handlers: ghost_totalDeposited, ghost_totalBorrowed, ghost_openPositions[], ghost_collateralPosted. Track every borrow and collateral deposit so you can assert that the protocol’s ledger matches your shadow one.

DEX / AMMs

Constant-function AMMs have mathematically provable invariants — this is where invariant testing shines brightest:

/// @notice The constant product k = x * y must never decrease
///         (except for fee withdrawals which are separately accounted for).
function invariant_constantProductNeverDecreases() public view {
    (uint256 r0, uint256 r1,) = pool.getReserves();
    uint256 k = r0 * r1;
    assertGe(k, handler.ghost_kMin(), "DEX-1: k decreased");
}

/// @notice Reserve ratio must stay within expected bounds after a swap.
function invariant_reservesSolvent() public view {
    (uint256 r0, uint256 r1,) = pool.getReserves();
    assertGt(r0, 0, "DEX-2: reserve0 drained");
    assertGt(r1, 0, "DEX-3: reserve1 drained");
}

/// @notice LP token supply must be backed by actual reserves.
function invariant_lpTokensBacked() public view {
    uint256 totalLp   = pool.totalSupply();
    (uint256 r0, uint256 r1,) = pool.getReserves();
    if (totalLp == 0) {
        assertEq(r0, 0);
        assertEq(r1, 0);
    }
}

/// @notice No single actor can extract more value than they put in.
function invariant_noValueExtraction() public view {
    address[] memory actors = handler.getActors();
    for (uint256 i; i < actors.length; i++) {
        int256 netFlow = handler.ghost_netAssetFlow(actors[i]);
        // netFlow = total out - total in; should be <= fees earned
        assertLe(netFlow, int256(handler.ghost_feesEarned(actors[i])), "DEX-4: value extracted");
    }
}

For DEX handlers, bound swap amounts to a fraction of current reserves so the fuzzer explores realistic slippage rather than draining the entire pool in one call (which would be a no-op in practice due to the invariant check).

---

How the Fuzzer Explores State Space

Understanding the exploration model helps you configure tests and interpret failures.

Under the hood, Foundry deploys your contracts, then runs many “runs” of random calls up to a certain “depth”. Each run is a sequence of up to depth random transactions. After each transaction, all invariant_ functions are checked against the new state.

The fuzzer maintains a dictionary — a pool of interesting values discovered during previous runs (addresses that were touched, storage values it observed, boundary values). It uses these to generate inputs more likely to interact meaningfully with the protocol rather than random garbage.

The fuzzing engine operates through a feedback loop where test execution results inform the generation of subsequent inputs. This approach ensures that the fuzzer doesn’t waste time on redundant test cases but instead focuses on exploring new areas of the input space more likely to reveal bugs. For invariant testing, Foundry maintains a pool of target contracts and available functions, randomly selecting and executing function calls while preserving state between calls.

Starting with Foundry v1.3.0, invariant tests come with coverage-guided fuzzing support that stores and mutates previously tested call sequences. This mode can be enabled by setting the corpus_dir config, which is the path on disk used to persist the corpus that generates new coverage.

Foundry also supports sampling typed storage values during invariant testing to generate more intelligent test inputs. This feature leverages contract storage layouts to understand the types of storage variables and sample appropriate values based on those types.

One critical subtlety: when implementing invariant tests, it is important to be aware that for each invariant_* function a different EVM executor is created, therefore invariants are not asserted against the same EVM state. This means that if invariant_A() and invariant_B() are defined, then invariant_B() will not be asserted against the EVM state of invariant_A(). If you need joint assertions, group them in a single function.

---

Configuring Runs, Depth, and Profiles

Regular invariant testing campaigns have two dimensions: runs — the number of times that a sequence of function calls is generated and run — and depth — the number of function calls made in a given run.

runs: The number of runs that must execute for each invariant test group (default value is 256). depth: The number of calls executed to attempt to break invariants in one run (default value is 15).

The product runs × depth is the total number of state-changing calls made. More depth is almost always more valuable than more runs for finding multi-step bugs — a depth of 500 with 100 runs will find more interesting sequences than a depth of 15 with 10,000 runs.

A production-grade foundry.toml with separate local and CI profiles:

[profile.default]
src     = "src"
test    = "test"
out     = "out"
libs    = ["lib"]

# Enable storage layout sampling for smarter fuzzing
extra_output = ["storageLayout"]

[profile.default.invariant]
runs           = 64
depth          = 32
fail_on_revert = true
shrink_run_limit = 1000

# CI profile: heavier, no debug output
[profile.ci.invariant]
runs             = 512
depth            = 256
fail_on_revert   = true
shrink_run_limit = 5000
corpus_dir       = "invariant-corpus"

[profile.ci.fuzz]
runs = 10_000

fail_on_revert: Fails the invariant fuzzing if a revert occurs (default value is false). Alternatively, these parameters can be set in environment variables, for example FOUNDRY_INVARIANT_RUNS=10000.

A good practice is to set show_metrics = true to get a breakdown of all handler function calls and which functions are reverting or getting discarded through the vm.assume cheatcode. In addition, with handlers, input parameters can be bounded to reasonable expected values such that fail_on_revert in foundry.toml can be set to true.

You can also configure individual tests inline using Forge config comments, without modifying foundry.toml:

/// forge-config: default.invariant.runs = 500
/// forge-config: default.invariant.depth = 100
/// forge-config: default.invariant.fail-on-revert = true
function invariant_totalSupplyMatchesSumOfBalances() public view {
    assertEq(token.totalSupply(), handler.ghost_totalMinted() - handler.ghost_totalBurned());
}

Inline config comments override foundry.toml for individual invariant functions without affecting the rest of the test suite. This is useful when a specific invariant needs a much higher run count to achieve meaningful coverage without slowing down the entire suite.

---

Foundry Invariant Testing Checklist

Handler design

• All state-mutating protocol functions are wrapped in handler functions
• Handler functions bound inputs with bound() or vm.assume() to exclude impossible states
• Ghost variables track aggregate state (total minted, total burned, sum of balances) for conservation invariants
• fail_on_revert = true is enabled once handlers are mature, to catch unexpected reverts

Invariant coverage

• At least one conservation invariant is defined (e.g., totalSupply == sum(balances))
• At least one solvency invariant is defined (e.g., totalCollateral >= totalDebt)
• Access control invariants are tested (e.g., no unprivileged address can mint)
• Rounding direction invariants are tested (e.g., previewWithdraw >= withdraw for same shares)

Configuration

• runs is set to at least 500 for core invariants
• depth is set to at least 100 to allow meaningful call sequences to develop
• show_metrics = true is enabled to verify handler call distribution is balanced
• Invariant tests run in CI on every PR touching core protocol logic

Debugging

• Failing sequences have been replayed with --rerun to confirm reproducibility
• Call sequences that break invariants have been reduced to minimal reproducers
• All invariant failures have been triaged before merging