A DeFi protocol can have clean, audited Solidity code and still lose millions. The reason is almost always the same: an economic invariant — a mathematical relationship that the protocol silently relies on to remain solvent — was violated. This “specification gap” is illustrated by protocols that have undergone numerous separate audits, where the code did exactly what the math allowed, but the math allowed for precision rounding errors that an attacker could exploit to manipulate invariants — the failure wasn’t in the code’s deviation from the spec, but in the spec’s deviation from economic reality.

This article walks through what economic invariants are, how they appear across every major DeFi primitive, how their violation manifests as exploits, and how to systematically identify and test them during a security audit.

What Is an Economic Invariant?

In mathematics, an invariant is a property of a system that remains unchanged under a defined set of transformations. In DeFi, an economic invariant is a mathematical relationship between protocol state variables that must hold true after every valid operation for the protocol to remain solvent, correct, and non-exploitable.

Invariants are conditions that must always be true under a certain set of well-defined assumptions. They are distinct from access-control checks or reentrancy guards — those are code-level properties. Economic invariants are system-level properties: they describe what the protocol promises about the relationship between funds, shares, debts, and reserves at any point in time.

Consider a simple token contract. Its economic invariant is obvious: the sum of all individual balances must equal the total supply. In an ERC-20 contract, an invariant would be that the sum of all balances in the contract should equal the total supply. Violate this, and you have either a mint bug or a burn bug — and an attacker who can exploit one has effectively printed money.

For complex DeFi systems, the invariants are far less obvious but far more consequential.

How to Identify Invariants

Identifying invariants during an audit is a process of asking the question: what mathematical relationship, if broken, would allow an attacker to extract more value than they put in? The process looks like this:

  1. Map all state variables that represent value: reserves, balances, shares, debts, collateral, accumulated fees.
  2. Enumerate all state-changing functions: deposits, withdrawals, swaps, borrows, liquidations, reward claims.
  3. Ask per-function: what should be conserved? What should strictly increase? What should strictly decrease?
  4. Ask cross-function: what global relationship must hold across all users and all time?
  5. Identify the invariant’s dependencies: what oracles, interest rate models, or external contracts does the invariant assume correct behavior from?

The invariants captured should drive a comprehensive testing suite. Unit and integration testing should lead to 100% coverage. But invariants deserve a separate class of test entirely — one that doesn’t just check a single call path, but verifies that the relationship holds after any arbitrary sequence of interactions.

AMM Invariants

The Constant Product Invariant (x·y = k)

The constant product AMM is a revolutionary piece of financial engineering — it elegantly solves the on-chain liquidity problem by replacing the complex, high-touch order book with a simple, passive liquidity pool governed by the x * y = k invariant.

Here, x and y are the two token reserves, and k is the product that must be preserved after every swap. Formally:

k_post = (x + Δx) * (y - Δy) ≥ k_pre

The ≥ rather than strict equality accounts for protocol fees: swap fees increase the reserves slightly, causing k to grow over time. For constant-product markets, k = x * y stays constant or increases slightly as fees accrue. More generally, the pool’s total value should not shrink under normal (non-exit) operations — “total liquidity / total LP supply” should never go down as a result of any operation, even after a liquidity exit.

The security implications of this invariant are profound. It means:

  • No single swap can drain a pool to zero (the hyperbola is asymptotic).
  • LP tokens are always backed by proportional reserves.
  • Any operation that artificially reduces reserves — without a commensurate trade — is an exploit.

A real-world example: the root cause of one exploit lay in the tokenomics design — burning tokens directly from the pool’s balance during sell operations, followed by an immediate call to sync. This directly reduced the pool’s token reserve, violating the constant product invariant (K = x * y) used in UniswapV2, and this broken invariant allowed the attacker to manipulate the pool’s pricing mechanism and extract significant profit.

The Constant Sum Invariant (x + y = k)

The constant sum model — used by stablecoin-optimized AMMs in their simplest form — preserves the sum of reserves rather than the product:

x + y = k  (constant sum)

This provides zero price impact within its range (ideal for pegged assets) but has a catastrophic flaw: unlike the constant product, the constant sum curve is a straight line, which means a pool can be fully drained of one asset. If you can swap all of token y for token x, the pool hits an edge condition. The invariant to check here is not just the sum equality, but that neither reserve drops to zero — a state that should trigger circuit breakers in any well-designed implementation.

Concentrated Liquidity Invariants (Uniswap v3)

Uniswap v3 introduced a far more complex invariant surface. Uniswap v3 introduced concentrated liquidity, allowing liquidity providers to allocate capital to bounded price intervals rather than over the full price range. This design increases capital efficiency but complicates both economic analysis and security reasoning: liquidity is now piecewise, tick-driven, and stateful.

Uniswap v3 can be conceptualized as using the following invariant: xy = k_n where the value of k changes depending on which tick range the current price p occupies.

Uniswap v3 pools consist of multiple “small” swap pools, each identified by a separate tick. Each of these “small” pools behaves like a Uniswap v2 pool with a constant product, having its own reserves, but with an important difference — the reserves of the tick are depletable, having maximum and minimum swap price and limited amounts of each token.

The invariants for concentrated liquidity are therefore:

  1. Per-tick invariant: within a tick range, x * y ≥ k_tick.
  2. Cross-tick consistency: the liquidity delta at each tick boundary must net to zero globally (ticks added equal ticks removed for any given position lifecycle).
  3. Fee accumulation monotonicity: feeGrowthGlobal must be non-decreasing.
  4. Position integrity: a position’s owed tokens must equal the fees accumulated in its range minus fees already collected.

Uniswap v3-style concentrated-liquidity AMMs can be effectively modeled as networks of priced timed automata and finite-state transducers, with positions as stateful objects whose behavior is driven by tick crossings. Within this view, important correctness questions such as cross-tick invariance, price-state reachability, and rounding-arbitrage absence become standard safety and liveness properties for which mature model-checking tools exist.

The tick arithmetic in v3 is the most dangerous surface: rounding in sqrtPrice calculations, incorrect handling of tick transitions, and off-by-one errors in boundary conditions have all been sources of audit findings.

Lending Protocol Solvency Invariants

Collateral ratio is the simplest important number in DeFi lending: the value of collateral divided by the value of debt. It exists because lending against volatile, on-chain assets requires a buffer between what is owed and what can realistically be recovered.

The core solvency invariants for lending protocols form a hierarchy:

Core invariants include: total borrows ≤ total collateral × collateral factor; sum of all debts ≤ sum of all deposits; and individual positions maintain health factor ≥ 1 (or are liquidated). These guarantee that depositors can always withdraw (subject to utilization), borrowers cannot extract unbacked value, and liquidations maintain system health.

Breaking this down into testable components:

Global solvency: totalBorrows ≤ totalDeposits at all times.

Per-position health: (collateralValue × collateralFactor) / debtValue ≥ 1.0 for every non-liquidated position.

Liquidation atomicity: the act of liquidating must strictly improve global solvency — a liquidator who repays debt must receive collateral of equal or lesser economic value at oracle prices (the bonus is funded by the borrower’s buffer, not the protocol).

Interest accrual correctness: as time passes, total debt grows (via interest), but it must never grow faster than the protocol’s interest income. The invariant totalDebt ≤ totalSupply + accruedProtocolFees must hold continuously.

The Cream Finance exploit demonstrated oracle-related insolvency: the attacker manipulated the oracle price of yUSD, borrowed against inflated collateral, and extracted value exceeding the true collateral worth. The solvency invariant (borrows ≤ collateral × factor) appeared maintained, but the collateral value itself was manipulated. The lesson: solvency depends on oracle integrity — verification must include oracle robustness.

In a formal verification engagement with Kamino Lending, a subtle precision loss issue in the exchange rate calculation allowed someone to redeem more collateral than they originally deposited — an edge case that, while not exploitable at the time, could become a risk in the future. This is a textbook example of a solvency invariant being violated by arithmetic rounding rather than logic error.

Staking and Reward Distribution Invariants

Staking and yield-distribution contracts carry their own invariant family, often underspecified in audits because they feel “simpler” than AMMs or lending. They are not.

Reward accounting invariants:

  • Total rewards distributed ≤ total rewards deposited (or emitted according to the emission schedule).
  • A user’s claimable rewards must equal their share of total emissions over the period they were staked.
  • rewardPerTokenStored must be non-decreasing.
  • Removing stake must never increase rewardPerTokenStored.

The classic vulnerability in this space is the reward-per-token rounding exploit: if rewardPerToken is computed as totalRewards / totalStaked, an attacker who briefly stakes a tiny amount (making totalStaked very small) can inflate their share of rewards per second.

Another critical invariant: no user should be able to claim more than once for the same epoch. Checkpoint-based reward systems that fail to properly update a user’s rewardDebt before transferring tokens are vulnerable to reentrancy-mediated double-claims, even in a post-ERC-777 world if the reward token itself has hooks.

LP token share invariants (ERC-4626 vaults):

  • totalAssets / totalSupply (the share price) must be non-decreasing under normal operation.
  • A deposit immediately followed by a withdrawal must return ≤ the deposited amount (no inflation attack).
  • The first-depositor invariant: totalSupply > 0 OR totalAssets == 0 — the “empty vault” state must be unreachable for a non-trivial amount, protecting against share-price manipulation via direct token transfers.

Within handler contracts for invariant testing, “ghost variables” can be tracked across multiple function calls to add additional information for invariant tests. A good example is summing all of the shares that each LP owns after depositing into an ERC-4626 token, and using that sum in the invariant (totalSupply == sumBalanceOf).

How Invariant Violations Manifest as Exploits

Every major AMM exploit ultimately violates one of these core properties. The violation path almost always follows one of these patterns:

1. Price manipulation via flash loans. The spot price of an AMM pool (reserveY / reserveX) is trivial to manipulate. An attacker can use a flash loan to execute a massive trade, momentarily shift the reserve ratio to a desired value, perform an action on another protocol that relies on this manipulated price, and then trade back to restore the original price — all within a single atomic transaction. This makes the instantaneous spot price of a simple AMM a fundamentally insecure price oracle, and using it as a source of truth for critical operations like issuing loans is one of the most common and devastating vulnerabilities in DeFi.

The invariant being violated here is the oracle integrity invariant of the lending protocol: the assumed property that collateralValue = oraclePrice × amount reflects true economic value. When the oracle is a manipulable AMM spot price, this assumption breaks.

2. Reserve manipulation via transfer tax / fee-on-transfer tokens. When a protocol assumes that token.transferFrom(user, pool, amount) results in the pool receiving exactly amount, but the token charges a fee on transfer, the pool’s internal accounting diverges from its actual balance. The x * y = k invariant holds for the recorded reserves, but not for the real reserves.

3. Rounding accumulation. The broader industry trend of identifying severe rounding issues confirms that arithmetic and correct precision are as critical as ever. If a protocol always rounds in favor of the user rather than the pool, small per-transaction gains accumulate. An attacker who can batch thousands of micro-transactions can drain meaningful value over time without any single transaction looking suspicious.

4. Composability invariant breaks. Real-world exploits regarding CPMM composability bugs arise due to violating two safety invariants. CPMM-Exploiter, a grammar-based fuzzer, uses fuzzing to find transactions that break these invariants, and then refines those transactions to make them profitable for the attacker. Composability means a protocol’s invariant can be violated not by attacking it directly, but by constructing a cross-protocol interaction sequence that leaves the invariant in a broken state.

Common themes in DeFi exploits include flash loan attacks, price oracle manipulation, and unexpected interaction effects between protocols.

Formal Verification vs. Fuzzing for Invariant Testing

Two primary methodologies exist for mechanically verifying invariants: formal verification and property-based fuzzing. They are complementary, not competitive.

Formal Verification

Formal verification applies mathematical proofs to ensure correctness and is used in 2025 for high-value contracts (e.g., core token bridges) with costs often exceeding $200,000.

Tools like the Certora Prover use a specification language (CVL) to express invariants as mathematical propositions, then apply symbolic execution to attempt to prove or disprove them across all possible inputs. The Certora team used their Certora Prover to identify an interesting issue in the Compound V3 Comet smart contracts that allowed a fully collateralized account to be liquidated. The root cause was using an 8-bit mask for a 16-bit vector — the mask remained zero for the higher bits in the vector, which skipped assets while calculating total collateral and resulted in the liquidation of a collateralized account.

The key advantage of formal verification is completeness: if the tool proves an invariant, it holds for all inputs, not just those the fuzzer happened to find. Fuzzing catches bugs. Formal verification proves their absence.

The key limitation: Formal Verification is often called the “gold standard,” but it is only as good as its specification. FV can prove that a withdraw() function only works if balance > amount. It cannot prove that the mathematical formula for calculating amount is economically sound under extreme market conditions.

Formal verification tools require a lot of domain-specific knowledge to be used effectively and require significant engineering efforts to apply. While formal verification tools are constantly improving — which reduces the engineering effort — none of the existing tools reach the ease of use of existing fuzzers.

Fuzzing

Invariant testing allows testing of aspects of a smart contract that unit tests will likely miss. Unit tests only cover properties specified in the test and nothing else. But with invariant testing, smart contracts are tried and tested under multiple random states to find flaws in the code. By testing these invariants, developers can catch potential issues that unit tests or manual code reviews may not detect.

The ecosystem offers several production-grade fuzzing tools:

  • Foundry (forge test --invariant): the most widely adopted, with excellent handler-based testing support.
  • Echidna: Trail of Bits’ property-based fuzzer, battle-tested across hundreds of production audits. Echidna can violate invariants in less than a minute on consumer hardware.
  • Medusa: a newer contender. Medusa is able to almost immediately break both simple and complex invariants in unguided basic mode.
  • Halmos: a symbolic execution tool that bridges fuzzing and formal verification. Halmos excels at arithmetic edge cases (overflow, rounding, precision loss), access control completeness, and state transition correctness — verifying invariants hold across all function calls.

The practical advice from the security community is clear: a layered approach works best — Slither static analysis for low-hanging fruit, Foundry fuzz tests for common edge cases, Halmos symbolic tests to prove arithmetic properties for all inputs, and Certora CVL specs to prove protocol-level invariants on critical paths.

Writing Foundry Invariant Tests

Invariant tests are stateful fuzz tests that assert “rules” which must always hold true, even after any sequence of contract calls. Foundry’s invariant engine works by calling randomly selected functions in a target contract (or handler) with fuzzed parameters, then checking that the invariant_* functions still return true after each call.

The Handler Pattern

An in-depth exploration of invariant testing in Foundry reveals how stateful fuzz testing verifies smart contract properties that must always remain true. The basic, often inefficient Open Testing approach should be contrasted with the more precise and powerful Handler-Based strategy for effective bug discovery.

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. Within handlers, “ghost variables” can be tracked across multiple function calls to add additional information for invariant tests.

Example 1: Constant Product AMM Invariant

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

/// @title AMMHandler
/// @notice Mediates all fuzzer interactions with the AMM pool,
///         bounding inputs to valid ranges and tracking ghost state.
contract AMMHandler is Test {
    SimpleAMM public amm;
    MockERC20 public tokenA;
    MockERC20 public tokenB;

    // Ghost variable: track deposited liquidity
    uint256 public ghost_totalLiquidityAdded;
    uint256 public ghost_totalLiquidityRemoved;

    constructor(SimpleAMM _amm, MockERC20 _tokenA, MockERC20 _tokenB) {
        amm = _amm;
        tokenA = _tokenA;
        tokenB = _tokenB;
        // Seed the handler with tokens
        tokenA.mint(address(this), 1_000_000e18);
        tokenB.mint(address(this), 1_000_000e18);
        tokenA.approve(address(amm), type(uint256).max);
        tokenB.approve(address(amm), type(uint256).max);
    }

    function swapAForB(uint256 amountIn) external {
        amountIn = bound(amountIn, 1, tokenA.balanceOf(address(this)));
        amm.swapAForB(amountIn);
    }

    function swapBForA(uint256 amountIn) external {
        amountIn = bound(amountIn, 1, tokenB.balanceOf(address(this)));
        amm.swapBForA(amountIn);
    }

    function addLiquidity(uint256 amountA, uint256 amountB) external {
        amountA = bound(amountA, 1, tokenA.balanceOf(address(this)));
        amountB = bound(amountB, 1, tokenB.balanceOf(address(this)));
        uint256 shares = amm.addLiquidity(amountA, amountB);
        ghost_totalLiquidityAdded += shares;
    }

    function removeLiquidity(uint256 shares) external {
        shares = bound(shares, 1, amm.balanceOf(address(this)));
        amm.removeLiquidity(shares);
        ghost_totalLiquidityRemoved += shares;
    }
}

/// @title AMMInvariantTest
/// @notice Invariant test suite for a constant-product AMM
contract AMMInvariantTest is StdInvariant, Test {
    SimpleAMM public amm;
    MockERC20 public tokenA;
    MockERC20 public tokenB;
    AMMHandler public handler;

    uint256 public initialK;

    function setUp() public {
        tokenA = new MockERC20("Token A", "TKNA");
        tokenB = new MockERC20("Token B", "TKNB");
        amm = new SimpleAMM(address(tokenA), address(tokenB));
        handler = new AMMHandler(amm, tokenA, tokenB);

        // Seed initial liquidity
        tokenA.mint(address(this), 100_000e18);
        tokenB.mint(address(this), 100_000e18);
        tokenA.approve(address(amm), type(uint256).max);
        tokenB.approve(address(amm), type(uint256).max);
        amm.addLiquidity(100_000e18, 100_000e18);

        initialK = amm.reserveA() * amm.reserveB();

        // Direct the fuzzer at the handler, not the AMM directly
        targetContract(address(handler));
    }

    /// @notice The product of reserves must never decrease below its
    ///         post-initialization value (fees can cause it to grow)
    function invariant_constantProductNeverDecreases() public view {
        uint256 currentK = amm.reserveA() * amm.reserveB();
        assertGe(currentK, initialK, "K invariant violated: reserves decreased");
    }

    /// @notice LP token supply must be consistent with ghost accounting
    function invariant_lpSupplyConsistency() public view {
        uint256 netShares = handler.ghost_totalLiquidityAdded() -
            handler.ghost_totalLiquidityRemoved();
        // Total supply should equal initial supply + net handler shares
        assertEq(
            amm.totalSupply(),
            1000e18 + netShares, // 1000e18 = initial LP shares to this
            "LP supply inconsistency"
        );
    }

    /// @notice Reserves must always be backed by real token balances
    function invariant_reservesSolvent() public view {
        assertLe(
            amm.reserveA(),
            tokenA.balanceOf(address(amm)),
            "ReserveA exceeds actual token balance"
        );
        assertLe(
            amm.reserveB(),
            tokenB.balanceOf(address(amm)),
            "ReserveB exceeds actual token balance"
        );
    }

    /// @notice Share price (k per LP token) must be non-decreasing
    function invariant_sharePriceNeverDecreases() public view {
        if (amm.totalSupply() == 0) return;
        uint256 kPerShare = (amm.reserveA() * amm.reserveB()) / amm.totalSupply();
        uint256 initialKPerShare = initialK / 1000e18;
        assertGe(kPerShare, initialKPerShare, "Share price decreased");
    }
}

Example 2: Lending Protocol Solvency Invariant

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

contract LendingHandler is Test {
    LendingPool public pool;
    MockERC20 public collateralToken;
    MockERC20 public borrowToken;
    MockOracle public oracle;

    // Ghost variables for cross-call accounting
    uint256 public ghost_totalDeposited;
    uint256 public ghost_totalWithdrawn;
    uint256 public ghost_totalBorrowed;
    uint256 public ghost_totalRepaid;

    address[] public actors;
    uint256 constant NUM_ACTORS = 5;

    constructor(
        LendingPool _pool,
        MockERC20 _collateral,
        MockERC20 _borrow,
        MockOracle _oracle
    ) {
        pool = _pool;
        collateralToken = _collateral;
        borrowToken = _borrow;
        oracle = _oracle;

        for (uint256 i = 0; i < NUM_ACTORS; i++) {
            address actor = address(uint160(i + 1));
            actors.push(actor);
            collateralToken.mint(actor, 10_000e18);
            borrowToken.mint(actor, 10_000e18);
            vm.prank(actor);
            collateralToken.approve(address(pool), type(uint256).max);
            vm.prank(actor);
            borrowToken.approve(address(pool), type(uint256).max);
        }
    }

    function depositCollateral(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % NUM_ACTORS];
        amount = bound(amount, 1, collateralToken.balanceOf(actor));
        vm.prank(actor);
        pool.depositCollateral(amount);
        ghost_totalDeposited += amount;
    }

    function borrow(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % NUM_ACTORS];
        uint256 maxBorrow = pool.maxBorrowAmount(actor);
        if (maxBorrow == 0) return;
        amount = bound(amount, 1, maxBorrow);
        vm.prank(actor);
        try pool.borrow(amount) {
            ghost_totalBorrowed += amount;
        } catch {}
    }

    function repay(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % NUM_ACTORS];
        uint256 debt = pool.debtOf(actor);
        if (debt == 0) return;
        amount = bound(amount, 1, debt);
        vm.prank(actor);
        pool.repay(amount);
        ghost_totalRepaid += amount;
    }

    function liquidate(uint256 actorSeed, uint256 targetSeed) external {
        address liquidator = actors[actorSeed % NUM_ACTORS];
        address target = actors[targetSeed % NUM_ACTORS];
        if (pool.healthFactor(target) >= 1e18) return;
        vm.prank(liquidator);
        try pool.liquidate(target) {} catch {}
    }
}

contract LendingInvariantTest is StdInvariant, Test {
    LendingPool public pool;
    MockERC20 public collateralToken;
    MockERC20 public borrowToken;
    MockOracle public oracle;
    LendingHandler public handler;

    function setUp() public {
        collateralToken = new MockERC20("Collateral", "COL");
        borrowToken = new MockERC20("Borrow", "BRW");
        oracle = new MockOracle();
        oracle.setPrice(address(collateralToken), 1e18); // $1 per token
        oracle.setPrice(address(borrowToken), 1e18);

        pool = new LendingPool(
            address(collateralToken),
            address(borrowToken),
            address(oracle),
            75e16 // 75% collateral factor
        );

        // Seed pool with borrow liquidity
        borrowToken.mint(address(this), 1_000_000e18);
        borrowToken.approve(address(pool), type(uint256).max);
        pool.supplyBorrowLiquidity(1_000_000e18);

        handler = new LendingHandler(pool, collateralToken, borrowToken, oracle);
        targetContract(address(handler));
    }

    /// @notice The protocol must always be solvent:
    ///         total collateral value >= total debt value
    function invariant_protocolSolvency() public view {
        uint256 totalCollateralValue = pool.getTotalCollateralValue();
        uint256 totalDebt = pool.getTotalDebt();
        assertGe(
            totalCollateralValue,
            totalDebt,
            "Protocol is insolvent: debt exceeds collateral"
        );
    }

    /// @notice Total borrows must never exceed supplied liquidity
    function invariant_borrowsDoNotExceedSupply() public view {
        assertLe(
            pool.getTotalDebt(),
            pool.getTotalSupplied(),
            "Borrows exceed total supply"
        );
    }

    /// @notice No position with health factor < 1 should exist unliquidated
    function invariant_noUnderwaterPositions() public view {
        address[] memory actors = handler.getActors();
        for (uint256 i = 0
; i < actors.length; i++) {
            address actor = actors[i];
            uint256 hf = lending.healthFactor(actor);
            // HF is scaled to 1e18; anything below 1e18 is liquidatable
            assertGe(hf, 1e18, string.concat("Unhealthy position: ", vm.toString(actor)));
        }
    }
}

This invariant, combined with a handler that calls liquidate as well as borrow and withdraw, forces the fuzzer to explore scenarios where liquidation is and is not triggered correctly. Any path through which an unhealthy position persists without being liquidatable is a direct protocol vulnerability.

Economic Invariant Audit Checklist

Conservation invariants

  • totalSupply == sum(balanceOf(all accounts)) for every token in the protocol
  • totalAssets >= sum(userShares * sharePrice) for every vault
  • totalDebt == sum(userDebt) for every lending pool
  • insuranceFund + collateralValue >= totalDebt at all times

Solvency invariants

  • No position with health factor < 1 can exist without being liquidatable
  • Liquidation always improves the health factor of the liquidated position
  • Bad debt cannot exceed the protocol’s insurance fund without triggering socialized loss

Monotonicity invariants

  • Share price is monotonically non-decreasing in a yield-bearing vault (absent slashing)
  • A user who deposits and immediately redeems receives at most their deposited amount
  • Accumulated interest never decreases

No-free-value invariants

  • No sequence of valid transactions produces net profit for an attacker without providing real capital
  • Flash loan callbacks cannot leave the protocol in a state that is more favorable to the attacker than before the flash loan

Fuzzer integration

  • Every invariant is implemented as a invariant_* function in a Foundry handler suite or an echidna_* property
  • Handlers cover all state-mutating protocol functions
  • Ghost variables track aggregate state for conservation checks
  • Campaigns run for at least 500 sequences × 100 depth before audit sign-off