AMM (Automated Market Maker)

spec · config

A constant-product market maker (x*y=k). No order book — traders swap against a liquidity pool. Price is determined by the reserve ratio, not by matching orders. This models Uniswap v2 and its forks (SushiSwap, PancakeSwap). Related designs include Curve (StableSwap invariant) and Balancer (generalized weighted pools).

graph LR
    subgraph Pool
        RA[Reserve A]
        RB[Reserve B]
        K["x * y = k"]
    end

    S1["Swap A for B"] -- "amtIn of A" --> RA
    RA -- "amtOut of B" --> S1
    RB -- "amtOut of B" --> S1

    S2["Swap B for A"] -- "amtIn of B" --> RB
    RB -- "amtOut of A" --> S2
    RA -- "amtOut of A" --> S2

    RA -.- K
    RB -.- K

Traders swap tokens against the pool. The output amount is computed from the constant-product formula: amtOut = reserveY * amtIn / (reserveX + amtIn) (minus fees). Larger swaps get worse prices (price impact). The pool always has liquidity — swaps never fail due to an empty book.

  • Constant product: reserveA * reserveB >= k (k grows from fees)
  • Price impact: larger swaps move the price more, getting worse effective rates
  • Fees: configurable (default 0.3%), accrue to the pool reserves
  • No order book: price is a function of reserves, not supply/demand matching

Verified properties

PropertyTypeDescription
ConstantProductInvariantInvariantreserveA * reserveB >= initial k (never decreases)
PositiveReservesInvariantPool reserves are always > 0
PositiveSwapOutputInvariantEvery swap produces output > 0
ConservationOfTokensInvariantTotal tokens in system (pool + all traders) is constant

Comparison properties (expected to fail)

Add as INVARIANT in AMM.cfg to see a counterexample:

PropertyDescription
AllSwapsSamePriceAll swaps get the same effective price (FAILS: AMM prices depend on swap size and reserve state — larger swaps get worse rates due to price impact. Contrast with BatchedAuction where UniformClearingPrice holds for all trades)