AMM and DEX Invariant Testing: Properties Every Swap Protocol Needs

By nican0r

If you're building or auditing an AMM, you already know the math matters. But knowing the math and proving it holds under adversarial conditions are two very different things. I've seen constant-product implementations that look perfect in unit tests blow up the moment a fuzzer throws unexpected sequences at them.

This guide covers the full property suite you need for AMM/DEX protocols — from the basics like x * y = k all the way to sandwich resistance and concentrated liquidity edge cases. We'll write real invariant tests you can drop into your test suite today.

The constant product invariant: it's not as simple as you think

Everyone knows the formula. x * y = k after fees. But here's what trips people up: k should only ever increase (from fees) or stay the same. It should never decrease unless liquidity is removed.

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

import {Test} from "forge-std/Test.sol";

contract AMMInvariantTest is Test {
    AMMPool pool;
    AMMHandler handler;

    function setUp() public {
        pool = new AMMPool();
        handler = new AMMHandler(pool);
        targetContract(address(handler));
    }

    /// @notice k must never decrease after swaps
    function invariant_constant_product_never_decreases() public view {
        uint256 reserveX = pool.reserveX();
        uint256 reserveY = pool.reserveY();
        uint256 currentK = reserveX * reserveY;
        assertGe(currentK, handler.lastRecordedK(), "k decreased after swap");
    }

    /// @notice Total supply of LP tokens tracks actual liquidity
    function invariant_lp_shares_backed() public view {
        uint256 reserveX = pool.reserveX();
        uint256 reserveY = pool.reserveY();
        if (pool.totalSupply() == 0) {
            assertEq(reserveX, 0, "Reserves exist without LP tokens");
            assertEq(reserveY, 0, "Reserves exist without LP tokens");
        } else {
            assertGt(reserveX, 0, "LP tokens exist without reserves");
            assertGt(reserveY, 0, "LP tokens exist without reserves");
        }
    }
}

The test above catches a surprisingly common bug: implementations that accidentally let k shrink due to rounding in the swap math. If you've read about rounding errors in DeFi, you know these tiny precision losses compound fast.

The no-free-tokens property

This one's non-negotiable. No sequence of actions should let a user extract more tokens than they deposited plus any legitimately earned fees. Sounds obvious, right? You'd be surprised how often fuzzing catches violations.

/// @notice No user can extract value without providing value
function invariant_no_free_tokens() public view {
    uint256 totalTokenXInPool = tokenX.balanceOf(address(pool));
    uint256 totalTokenYInPool = tokenY.balanceOf(address(pool));

    // Pool's actual balances must match or exceed tracked reserves
    assertGe(
        totalTokenXInPool,
        pool.reserveX(),
        "Pool tokenX balance less than tracked reserve"
    );
    assertGe(
        totalTokenYInPool,
        pool.reserveY(),
        "Pool tokenY balance less than tracked reserve"
    );
}

/// @notice Sum of all LP shares equals totalSupply
function invariant_lp_share_accounting() public view {
    uint256 trackedShares = handler.sumOfAllUserShares();
    assertEq(
        trackedShares,
        pool.totalSupply(),
        "Ghost variable share sum != totalSupply"
    );
}

The ghost variable pattern here is key. Your handler tracks every user's LP balance in a side mapping, and the invariant verifies the pool's internal accounting matches. This catches double-mint bugs and incorrect burn calculations that unit tests almost never find.

Fee accounting properties

Fees are where AMM bugs love to hide. The properties you need:

1. Fee collection monotonicity: accumulated fees never decrease
2. Fee bounds: actual fee charged falls within the configured range
3. Fee distribution proportionality: LPs get fees proportional to their share

/// @notice Fees collected must be monotonically increasing
function invariant_fees_monotonic() public view {
    assertGe(
        pool.accumulatedFeesX(),
        handler.previousFeesX(),
        "FeesX decreased"
    );
    assertGe(
        pool.accumulatedFeesY(),
        handler.previousFeesY(),
        "FeesY decreased"
    );
}

/// @notice Every swap must charge fee within configured bounds
/// (Checked per-call in handler, not as a global invariant)
function assertFeeInBounds(
    uint256 amountIn,
    uint256 feeCharged
) internal view {
    uint256 expectedMinFee = (amountIn * pool.feeRate()) / 10000;
    // Allow 1 wei tolerance for rounding
    assertGe(
        feeCharged + 1,
        expectedMinFee,
        "Fee charged below minimum"
    );
    assertLe(
        feeCharged,
        expectedMinFee + 1,
        "Fee charged above maximum"
    );
}

Liquidity provider share accounting

LPs need guarantees. When you add liquidity, you get shares proportional to your contribution. When you remove it, you get tokens proportional to your shares. Any deviation is a bug.

/// @notice Adding then removing liquidity should return ≥ original amount minus fees
function test_liquidity_round_trip(
    uint256 amountX,
    uint256 amountY
) public {
    amountX = bound(amountX, 1e18, 1e24);
    amountY = bound(amountY, 1e18, 1e24);

    uint256 beforeX = tokenX.balanceOf(address(this));
    uint256 beforeY = tokenY.balanceOf(address(this));

    uint256 shares = pool.addLiquidity(amountX, amountY);
    (uint256 returnedX, uint256 returnedY) = pool.removeLiquidity(shares);

    // Should get back at least 99.9% (accounting for rounding)
    assertGe(returnedX, (amountX * 999) / 1000, "Lost too much tokenX");
    assertGe(returnedY, (amountY * 999) / 1000, "Lost too much tokenY");
}

That 0.1% tolerance handles legitimate rounding. If you're losing more than that on a round trip with no swaps in between, something's wrong with your mint/burn math.

Slippage bounds and price impact

Slippage properties protect users from getting wrecked on large swaps. The key property: actual execution price must fall within the slippage tolerance the user specified.

/// @notice Swap output must respect minimum output (slippage bound)
function test_slippage_respected(
    uint256 amountIn,
    uint256 minOut
) public {
    amountIn = bound(amountIn, 1e15, pool.reserveX() / 10);
    uint256 expectedOut = pool.getAmountOut(amountIn);
    minOut = bound(minOut, 1, expectedOut);

    uint256 actualOut = pool.swap(
        address(tokenX),
        amountIn,
        minOut
    );
    assertGe(actualOut, minOut, "Slippage bound violated");
}

/// @notice Price impact must be proportional to trade size
function invariant_price_impact_bounded() public view {
    // After any swap, the price shouldn't move more than
    // the proportion of reserves consumed
    uint256 priceRatio = (pool.reserveX() * 1e18) / pool.reserveY();
    uint256 deviation = priceRatio > handler.initialPriceRatio()
        ? priceRatio - handler.initialPriceRatio()
        : handler.initialPriceRatio() - priceRatio;

    // Price can't deviate more than the total % of reserves swapped
    assertLe(
        deviation,
        handler.totalVolumeAsPercentOfReserves(),
        "Price impact exceeds theoretical maximum"
    );
}

Sandwich resistance properties

Sandwich attacks are the bane of on-chain trading. While you can't fully prevent them at the AMM level, you can write properties that verify your protocol's defenses work.

/// @notice A frontrun-swap-backrun sequence shouldn't profit the attacker
/// more than the fee they paid
function test_sandwich_resistance(
    uint256 victimAmount,
    uint256 attackerAmount
) public {
    victimAmount = bound(victimAmount, 1e18, pool.reserveX() / 20);
    attackerAmount = bound(attackerAmount, 1e18, pool.reserveX() / 10);

    uint256 attackerBalanceBefore = tokenY.balanceOf(attacker);

    // Attacker frontrun
    vm.prank(attacker);
    pool.swap(address(tokenX), attackerAmount, 0);

    // Victim swap
    vm.prank(victim);
    pool.swap(address(tokenX), victimAmount, 0);

    // Attacker backrun - swap back
    vm.prank(attacker);
    uint256 tokenXBack = pool.swap(
        address(tokenY),
        tokenY.balanceOf(attacker) - attackerBalanceBefore,
        0
    );

    // Attacker shouldn't profit after fees
    assertLe(
        tokenXBack,
        attackerAmount,
        "Sandwich attack profitable after fees"
    );
}

This property won't hold for all AMM designs — concentrated liquidity pools with tight ranges can actually make sandwiching more profitable. Which brings us to...

Concentrated liquidity: how properties change for V3-style AMMs

Concentrated liquidity changes everything about your property suite. The constant product formula still applies, but only within each tick range. Here's what you need to add:

Tick-level properties

/// @notice Liquidity must be consistent across tick boundaries
function invariant_tick_liquidity_consistency() public view {
    int24 currentTick = pool.currentTick();
    uint128 activeLiquidity = pool.liquidity();

    // Sum of all positions overlapping current tick must equal active liquidity
    uint128 sumOfPositions = handler.sumLiquidityAtTick(currentTick);
    assertEq(
        activeLiquidity,
        sumOfPositions,
        "Active liquidity mismatch at current tick"
    );
}

/// @notice Crossing a tick must update liquidity by exactly the tick's net value
function invariant_tick_crossing_correctness() public view {
    // After each swap that crosses a tick, verify:
    // new_liquidity = old_liquidity + tick.liquidityNet
    if (handler.lastSwapCrossedTick()) {
        int24 crossedTick = handler.lastCrossedTick();
        int128 liquidityNet = pool.ticks(crossedTick).liquidityNet;
        assertEq(
            int128(pool.liquidity()),
            int128(handler.liquidityBeforeCross()) + liquidityNet,
            "Tick crossing liquidity update incorrect"
        );
    }
}

Position range properties

For V3-style pools, each LP position has a range. Properties must verify:

• Range boundaries are valid: lower tick < upper tick, both on valid tick spacing
• Fees accrue only within range: out-of-range positions don't earn fees
• Fee growth tracking is correct: feeGrowthInside calculations match actual fees
• Position liquidity sums to tick liquidity: no liquidity appears from nowhere

/// @notice Out-of-range positions must not earn fees
function invariant_no_fees_outside_range() public view {
    for (uint256 i = 0; i < handler.positionCount(); i++) {
        Position memory pos = handler.getPosition(i);
        int24 currentTick = pool.currentTick();

        if (currentTick < pos.tickLower || currentTick >= pos.tickUpper) {
            // Position is out of range, fees shouldn't have changed
            assertEq(
                pos.currentFees,
                pos.feesAtLastCheck,
                "Out-of-range position earned fees"
            );
        }
    }
}

Building your handler

The handler is where the magic happens. It's the contract that the fuzzer calls to interact with your AMM. A good handler for AMM testing needs these actions:

1. swap, both directions, random amounts
2. addLiquidity, random amounts (and random ranges for V3)
3. removeLiquidity, random shares/positions
4. collectFees, for V3-style pools
5. donate, if supported, to test fee distribution

Each action should update ghost variables that your invariants check against. Track cumulative volumes along with fee totals and the last-known k value.

Common bugs these properties catch

After running these property suites across dozens of AMM forks, here's what comes up most:

1. Rounding in swap math. The output calculation rounds in the wrong direction, letting users extract 1 wei per swap. Over millions of swaps, this drains the pool. The k monotonicity invariant catches this instantly.

2. First depositor attack. The first LP can manipulate the initial price ratio to steal from subsequent depositors. The no-free-tokens property catches this when the fuzzer tries deposit sequences.

3. Fee-on-transfer token handling. Pool assumes it received the full amountIn but the actual balance increased by less. The reserve-vs-balance invariant catches this.

4. LP share inflation. Minting shares without proportional deposits. The share accounting invariant catches it.

If you want to understand why invariant testing matters for DeFi security, these bugs are exactly why. Unit tests check happy paths. Invariant tests check every path.

Putting it all together

Start with the three core invariants: constant product monotonicity, no-free-tokens, and LP share accounting. These catch 80% of AMM bugs. Then add fee accounting and slippage bounds. Finally, if you're doing concentrated liquidity, add the tick-level properties.

Don't try to write all properties on day one. Build them incrementally, run the fuzzer after each addition, and fix what breaks. Your coverage-guided fuzzer will find the interesting paths. Your job is to define what "correct" means.

For a deeper look at property design patterns across DeFi protocols, check out property design patterns for DeFi lending. And if you haven't written your first invariant test yet, start with how to write your first invariant test.

---

Want a professional property suite for your AMM protocol? Request an Audit or Try Recon Pro to generate invariant tests automatically.