Specifying Uniswap: A Worked Formal Specification

Why specify something already this well understood

A specification is not documentation of code that exists. It is the artefact that sits between a design intention and an implementation, and it either makes the system's properties checkable or it does not. Specifying a protocol nobody disputes is the cleanest way to show what the document is supposed to do, because no argument about the mechanism gets in the way of the argument about the method.

The structure below is the one I use on systems that do not yet exist: decompose the state, map the mechanisms over it, then derive each state transition and state its invariants explicitly.

State

Four state layers, kept separate on purpose

The separation is the load-bearing decision. Collapse these and you lose the ability to say which agent knows what.

Global state

The information required to maintain an active pool: quantities $X$ and $Y$ of each asset, and the supply $S$ of tokens representing rights to pool liquidity — all over $mathbb{R}_{+}$ .

Stateful parameters and metrics

Parameters carry units, which is where most informal specifications go wrong: gas amount $gamma$ in $G_{mathrm{transaction}}$ , gas price $c$ in $mathrm{ETH}/G_{mathrm{transaction}}$ , and swap fee $phi$ as a rate. Metrics are derived, not stored:

P = \frac{X}{Y}

K = X \cdot Y

$P$ is the market price of asset 2 in the numeraire; $K$ is the invariant the pool quantities always adhere to.

Local state — and the inside/outside distinction

Local state is what an address holds: $x$ , $y$ , $s$ . It also carries each agent's private price beliefs $hat{ ho}_1, hat{ ho}_2$ , explicitly tagged as inside versus outside information.

Why belief is part of the state. Without it there is no way to express why anyone trades. A pool with no belief heterogeneity has no order flow, and a specification that cannot represent the reason for a transaction cannot be simulated against one.

Exogenous state

Not part of the system, but intrinsic to any dynamic model of it: assumed global prices $ho_1, ho_2$ in ETH and $ho_e$ in USD. Naming these as exogenous is what stops a model from quietly assuming its own price process.

Mechanisms

Three transitions, each with its invariant

Every mechanism declares what it preserves. That declaration is the specification's actual content.

Add liquidity — preserves price

Takes $Delta x$ and returns the $Delta y$ that must accompany it so the price is unchanged:

f_{\mathrm{add}}(\Delta x, P) = \Delta y \qquad \Rightarrow \qquad P^{+} = P

The invariant moves, and that is the point:

(X + \Delta x)(Y + \Delta y) = K^{+}

Shares are issued on the linear proportion of the contribution, which is what keeps ownership claims consistent across deposits:

\Delta s = S \cdot \frac{\Delta x}{X}

Resolving the global state:

X^{+} = X + \Delta x, \qquad Y^{+} = Y + \Delta y, \qquad S^{+} = S + \Delta s

Locally $x^{+} = x - Delta x$ and $y^{+} = y - Delta y$ , subject to $x geq Delta x$ and $y geq Delta y$ — preconditions belong in the specification, not in the implementation's error handling.

Withdraw liquidity — also preserves price

The symmetric operation. Burning $Delta s$ returns a pro-rata share of both reserves:

\Delta x = X \cdot \frac{\Delta s}{S}, \qquad \Delta y = Y \cdot \frac{\Delta s}{S}

Price is again held constant and $K$ falls. Add and withdraw are the two mechanisms that move the invariant without moving the price; swap is the one that does the opposite.

Swap — preserves the invariant, moves the price

The constant product is what is held fixed here:

X \cdot Y = (X + \Delta x)(Y - \Delta y) = K

Which fixes the output for a given input:

\Delta y = \frac{\frac{\Delta x}{X}(1 - P)}{1 + \frac{\Delta x}{X}(1 - P)} \cdot Y

And the price resolves to a new value:

f_P(X^{+}, Y^{+}) = P^{+}

The whole design in one line. Liquidity operations hold price and move

K

; trades hold

K

and move price. Every property people later argue about — slippage, impermanent loss, capital efficiency — follows from that split.

Actors

The action space

Roles drive mechanisms

A state machine with no actors is not a model of anything. The specification closes by assigning mechanisms to roles — an operational trader swapping in and out, an arbitrage trader closing the gap between $P$ and the exogenous $ho$ , and liquidity providers adding and withdrawing.

Once roles are attached, the specification is executable: each role has a feasible action set over the state, which is exactly what a simulation needs to be written against.

What this method buys

Properties become checkable. "Price is preserved" is a claim you can test, not a sentence in a blog post.
Preconditions surface early. The balance constraints appear in the specification rather than as a revert message.
Simulation is a translation, not a redesign. The state decomposition maps directly onto a cadCAD model.
Disagreement gets localised. Arguments become arguments about a named mechanism's invariant, which is a much shorter conversation.