Formal Market Mechanisms

A collection of TLA+ specifications that formally verify and compare market mechanisms (CLOBs, batch auctions, AMMs, and privacy-preserving dark pools) across correctness, fairness, MEV resistance, and decentralizability.

graph LR
    CLOB[CentralizedCLOB<br/><font size = '-1'>immediacy</font>] --> DCLOB[DecentralizedCLOB<br/><font size = '-1'>multi-node</font>]
    BA[BatchedAuction<br/><font size = '-1'>fairness</font>] -->|sealed bids| ZK[ZKDarkPool<br/><font size = '-1'>privacy</font>]
    ZK -->|pair hiding| SDEX[ShieldedDEX<br/><font size = '-1'>full privacy</font>]
    BA -.->|refinement proof| ZK
    AS[ShieldedAtomicSwap<br/><font size = '-1'>P2P settlement<br/>cross-chain native</font>]
    AMM[AMM<br/><font size = '-1'>always-on liquidity<br/>comparison baseline</font>]

7 mechanism specs: CentralizedCLOB · BatchedAuction · AMM · ZKDarkPool · ShieldedDEX · ShieldedAtomicSwap · DecentralizedCLOB

7 attack/economic/proof specs: SandwichAttack · FrontRunning · LatencyArbitrage · WashTrading · ImpermanentLoss · CrossVenueArbitrage · ZKRefinement

All results are TLC-verified — not just argued. See the Conclusions chapter for the full summary of findings.

For an accessible introduction to why this matters, read the blog post.

CentralizedCLOB

_{spec · config}

A continuous limit order book with a single matching engine. Orders are matched immediately using price-time priority. This models traditional exchanges like NYSE, NASDAQ, and centralized crypto exchanges (Binance, Coinbase).

graph LR
    subgraph Order Book
        BB[Buy Book<br/>sorted by price desc]
        SB[Sell Book<br/>sorted by price asc]
    end

    O1[Submit Buy] --> BB
    O2[Submit Sell] --> SB

    BB -- "best bid >= best ask" --> ME{Match Engine}
    SB -- "best bid >= best ask" --> ME

    ME -- "fill at ask price" --> T[Trade]
    ME -- "partial fill" --> BB
    ME -- "partial fill" --> SB

Each order is matched immediately on arrival. If no match is possible (e.g., a buy at 10 when the best ask is 12), the order rests on the book until a compatible order arrives. When a match occurs, the trade executes at the resting order's price — the order that was already on the book. Different trades can execute at different prices (enabling spread arbitrage).

• Matching: best bid vs best ask, executes at the price of the order already on the book
• Partial fills: smaller side is fully filled, larger side's quantity is reduced
• Self-trade prevention: a trader cannot match against themselves

Verified properties

Comparison properties (expected to fail)

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

BatchedAuction

_{spec · config}

A periodic auction that collects orders over a batch window, then clears all at a single uniform price that maximizes traded volume. This models systems like Penumbra (sealed-bid batch auctions with privacy on Cosmos), CoW Protocol (batch auctions for MEV protection), and NYSE/NASDAQ opening/closing auctions. The academic foundation is Budish, Cramton, and Shim's "The High-Frequency Trading Arms Race" (2015), which proposes frequent batch auctions to eliminate the latency arms race.

Because OrderingIndependence is verified, batch auctions are safe to decentralize — validators only need to agree on the set of orders, not their sequence. This is why Penumbra and CoW Protocol can run batch auctions across distributed validators without the consensus problems that plague decentralized CLOBs.

graph LR
    subgraph Collecting
        BO[Buy Orders]
        SO[Sell Orders]
    end

    O1[Submit Buy] --> BO
    O2[Submit Sell] --> SO

    BO --> CB[Close Batch]
    SO --> CB

    subgraph Clearing
        CB --> D[Demand Curve]
        CB --> S[Supply Curve]
        D --> CP[Clearing Price<br/>max volume]
        S --> CP
    end

    CP -- "all at uniform price" --> T[Trades]
    T --> R[Reset]
    R -. "next batch" .-> BO

Orders accumulate during the collection phase without matching. When the batch closes, a single clearing price is computed that maximizes traded volume. All trades execute at this uniform price — no spread to capture.

• Collection phase: orders accumulate without matching
• Clearing phase: compute clearing price from aggregate supply/demand curves, fill eligible orders at the uniform price
• Self-trade prevention: buyer-seller pairs with the same trader are skipped during clearing

Verified properties

All 6 invariants above are proven to carry over unchanged when privacy is added — see ZKRefinement.

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

Comparison properties (expected to fail)

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

ZKDarkPool

_{spec · config}

A sealed-bid batch auction with commit-reveal protocol — also known as a hidden batch auction, encrypted batch auction, or sealed-bid batch auction. This is not a different clearing mechanism from BatchedAuction: the clearing logic is identical (uniform price, maximum volume). The difference is an information-hiding layer: orders are sealed during collection and destroyed after clearing. All BatchedAuction invariants pass unchanged here, confirming they are structurally the same mechanism — privacy adds MEV resistance on top without altering correctness.

This models privacy-preserving DEXs like Penumbra (sealed-bid batch auctions with shielded transactions on Cosmos), Renegade (MPC-based dark pool for on-chain private matching), and partially MEV Blocker / MEV Share (encrypted mempools). The ZKRefinement proof formally confirms that all BatchedAuction invariants carry over — privacy is a pure addition.

sequenceDiagram
    participant T1 as Trader 1
    participant T2 as Trader 2
    participant DP as Dark Pool
    participant ZK as ZK Verifier

    Note over DP: Phase 1: COMMIT

    T1->>DP: sealed buy order (hidden)
    T2->>DP: sealed sell order (hidden)
    Note over T1,T2: Orders invisible to each other<br/>(cryptographic commitments)

    Note over DP: Phase 2: CLEAR

    DP->>DP: reveal & clear at uniform price
    DP->>ZK: prove clearing correctness
    ZK->>DP: ✓ valid

    Note over DP: Phase 3: DONE

    DP->>DP: destroy individual orders
    DP->>T1: your fill: qty @ clearing price
    DP->>T2: your fill: qty @ clearing price

    Note over T1,T2: Only clearing price + fills retained<br/>Individual orders destroyed (post-trade privacy)

Three phases enforce privacy structurally:

1. Commit: traders submit sealed orders — no visibility of others' orders (modeled as nondeterministic choice independent of other orders)
2. Clear: orders revealed, uniform-price batch clearing (same algorithm as BatchedAuction)
3. Done: individual orders destroyed, only clearing price + fills retained (ZK proofs verify correctness)

• Pre-trade privacy: order contents hidden during commit phase
• Commitment binding: orders cannot be modified after commit
• Post-trade privacy: individual orders destroyed after clearing
• MEV elimination: sealed bids + uniform price = zero spread to exploit = sandwich attacks impossible

Verified properties

ShieldedDEX

_{spec · config}

A multi-asset shielded exchange where even the asset pair is hidden — not just order contents. Inspired by Zcash Shielded Assets (ZIP-226/227): custom tokens issued within the shielded pool inherit Zcash's privacy guarantees, making transfers of different asset types indistinguishable on-chain. Also related to Penumbra's multi-asset shielded pools and Anoma's intent-centric privacy architecture.

This is a genuinely new mechanism type, not a formalization of an existing design. It extends ZKDarkPool from single-pair to multi-pair with asset-type privacy.

How it extends ZKDarkPool

ZKDarkPool operates on a single trading pair — one buy book and one sell book. Everyone knows which market they're in; the privacy covers order contents (price, quantity, identity) but not the pair itself.

ShieldedDEX maintains one order book per pair. With two pairs (e.g., ZEC/USDC and ETH/USDC), the state looks like:

ZKDarkPool (single pair):
  buyOrders  = <<order1, order2>>
  sellOrders = <<order3>>

ShieldedDEX (multi-pair):
  buyOrders  = [ZEC/USDC ↦ <<order1>>,  ETH/USDC ↦ <<order3>>]
  sellOrders = [ZEC/USDC ↦ <<order2>>,  ETH/USDC ↦ <<order4>>]

The clearing algorithm is identical — uniform price, maximum volume — but parameterized per pair. Each pair clears independently with its own price (CrossPairIsolation verified).

The privacy extension: when a trader submits a commitment, the pair assignment is hidden. An observer sees 4 commitments arrive but cannot tell which pair each targets — they could all be for the same pair, or spread across pairs. After clearing, all order books across all pairs are destroyed. The observer never learns which pairs were active, how many orders each received, or at what prices they cleared.

This is what makes asset-targeted attacks impossible: you can't sandwich a specific pair if you can't identify which pair to target.

Implementation status

Zcash's ZSA ZIPs (226/227) define how to issue and transfer custom tokens privately, but no matching engine exists in the Zcash protocol. A ShieldedDEX would require additional protocol work:

Possible paths to implementation:

• Consensus-layer ZIP — new transaction types for order commitments + consensus rule for batch clearing. Most secure, hardest to deploy.
• Layer 2 / sidechain — batch clearing off-chain, settlement on Zcash via shielded transfers. Easier to deploy, weaker trust assumptions.
• Smart contract layer — if Zcash gains programmability, ShieldedDEX could be a contract on the shielded pool.

How ShieldedDEX differs from existing systems

Penumbra hides the swapper's identity but the trading pair and amounts are public (the Swap action includes the TradingPair in cleartext). An attacker can see which markets are active and target them. Anoma delegates matching to solvers who need to see intent contents to construct valid solutions — private solving is a research goal, not a deployed feature. The solver role is permissionless (anyone can run one), but a solver is structurally required for trading. ShieldedDEX occupies a design point neither system has explored: pair-hiding with solver-free deterministic clearing.

What's novel (and what isn't)

The clearing mechanism itself is a batch auction applied per-pair — not a new algorithm. The privacy model is at the mechanism design level, not the cryptographic level (we don't specify ZK circuits). What is new:

1. Pair-hiding + deterministic clearing — no existing system combines these. Penumbra has deterministic clearing but public pairs. Anoma has privacy but trusted solvers. This is a previously unoccupied design point.
2. Formal proof: asset-type privacy prevents asset-targeted attacks — the only mechanism in our suite to resist all 6 attack categories (6/6 vs 5/6 for ZKDarkPool/BatchedAuction). TLC-verified, not argued.
3. Formal proof: privacy does NOT fix the impossibility triangle — a negative result with concrete counterexample (P1@1, P2@2 with no correction). The NoImmediacy invariant confirms batching still sacrifices immediacy regardless of privacy.
4. The 4th dimension: privacy vs price discovery — extends the impossibility triangle to a tetrahedron. Full asset-type privacy eliminates cross-pair arbitrage, which means price information doesn't propagate across pairs. This tradeoff has not been formalized before.

This spec formalizes the mechanism design that Zcash's ZSA infrastructure makes possible — a blueprint for what could be built once the protocol supports it.

Use cases

ShieldedDEX is not better for everyone — it trades immediacy and price discovery for privacy and MEV resistance. It's suited for scenarios where what you're trading is as sensitive as how much.

Where ShieldedDEX wins:

• Institutional portfolio rebalancing — a fund selling token X for token Y doesn't want the market to know which pairs they're active in. On Penumbra, observers see "someone is trading X/Y" and can front-run that market. On ShieldedDEX, they see only an opaque commitment.
• DAO treasury operations — a DAO diversifying from token A to token B. If the pair is visible, the market front-runs the diversification before the DAO can execute.
• Jurisdictional sensitivity — in some contexts, which asset you trade reveals more than the amount. Pair-hiding prevents asset-targeted surveillance.
• MEV-free trading without trusting anyone — Anoma hides intents but the solver sees them. Flashbots MEV Share requires trusting the builder. ShieldedDEX has no trusted party — deterministic clearing means validators verify correctness without seeing contents or pairs.

Where other mechanisms are better:

The short version: if you only need to hide how much you're trading, Penumbra already works. ShieldedDEX is for when you need to hide what you're trading.

Mechanism diagram

sequenceDiagram
    participant T1 as Trader 1
    participant T2 as Trader 2
    participant S as Shielded DEX
    participant O as Observer

    Note over S: COMMIT PHASE

    T1->>S: shielded commitment<br/>(pair hidden, contents hidden)
    T2->>S: shielded commitment<br/>(pair hidden, contents hidden)
    T1->>S: shielded commitment
    T2->>S: shielded commitment

    Note over O: sees: 4 commitments<br/>can't tell: which pairs,<br/>which directions, what prices

    Note over S: CLEAR PHASE (per-pair, isolated)

    S->>S: clear Pair 1 @ price 1
    S->>S: clear Pair 2 @ price 2

    Note over O: sees: clearing happened<br/>can't tell: which pairs cleared,<br/>at what prices, or how many pairs

    Note over S: DONE: all orders destroyed

    S->>T1: your fills (pair-specific)
    S->>T2: your fills (pair-specific)

    Note over O: cross-pair prices diverged<br/>(1 vs 2) but no one can<br/>see it to arbitrage

Observer information visibility

What an on-chain observer learns:

ShieldedDEX reveals strictly less information than every other mechanism. The rightmost column has the most No entries — this is the formal basis for the claim that it provides the strongest privacy guarantees in our suite.

The impossibility triangle is NOT fixed

ShieldedDEX still uses batch clearing, so it still sacrifices immediacy and always-on liquidity. Privacy adds a 4th dimension to the tradeoff space:

        Fairness ── privacy axis ── Privacy
           |                           |
    Immediacy ──────────────── Liquidity

The new tradeoff: privacy vs price discovery. Full asset-type privacy means no one can see cross-pair price divergence, so no one can arbitrage it. Price information doesn't propagate across pairs.

Verified properties (48,065 states)

Price discovery property (expected to fail)

Add as INVARIANT to see counterexample:

ShieldedAtomicSwap

_{spec · config}

A shielded atomic swap: P2P cross-chain settlement with unlinkability. Standard HTLCs have a known privacy flaw — the same hash H appears on both chains, allowing an observer to link the two legs of the swap. Even on privacy chains like Zcash, the HTLC hash pattern leaks cross-chain linkage.

ShieldedAtomicSwap replaces the hash reveal with a ZK proof of preimage knowledge. Each leg uses a different commitment on-chain, but the ZK proof guarantees they correspond to the same secret. An observer sees two independent shielded transactions — unlinkable.

How it differs from ShieldedDEX

Use cases

ShieldedAtomicSwap is not an exchange — it's private settlement between two parties who already agreed on terms. It trades price discovery for trustless cross-chain execution without linkability.

Where ShieldedAtomicSwap wins:

• Cross-chain swaps without bridges — bridges are the #1 hack target in crypto. Atomic swaps eliminate the bridge entirely — no custodian, no multisig, no wrapped tokens. Each party locks on their own chain and claims with a ZK proof.
• OTC trades between known counterparties — two parties who already agreed on a price (e.g., institutional OTC, treasury-to-treasury). They don't need price discovery — they need private, trustless settlement.
• Privacy-preserving cross-chain migration — moving value from one chain to another without leaving a linkable trail. Standard HTLCs leak the link via the shared hash. Shielded swaps break that link.
• Small P2P trades — no minimum batch size, no liquidity pool needed, no fees beyond gas. Two people can swap any amount directly.

Where other mechanisms are better:

Protocol

sequenceDiagram
    participant A as Alice<br/>(has asset A on Chain 1)
    participant C1 as Chain 1
    participant C2 as Chain 2
    participant B as Bob<br/>(has asset B on Chain 2)
    participant O as Observer

    Note over A,B: AGREE (off-chain, P2P)
    A-->>B: negotiate terms

    Note over A,B: LOCK

    A->>C1: lock A with shielded commitment C1
    Note over O: sees: shielded_lock on Chain 1

    B->>C2: lock B with shielded commitment C2
    Note over O: sees: shielded_lock on Chain 2<br/>C1 ≠ C2 — CANNOT link them

    Note over A,B: CLAIM

    A->>C2: claim B with ZK proof (not hash reveal)
    Note over O: sees: shielded_claim on Chain 2<br/>no secret revealed on-chain

    B->>C1: claim A with ZK proof
    Note over O: sees: shielded_claim on Chain 1<br/>still cannot link to Chain 2

    Note over A,B: DONE — swap complete
    Note over O: saw 4 independent shielded txs<br/>cannot determine they are related

Standard HTLC vs Shielded

Zcash protocol changes needed

Verified properties (32 states)

Properties expected to fail

Add as INVARIANT to see counterexamples:

The liveness vs safety tradeoff

The BobCanLose counterexample reveals a fundamental tradeoff in atomic swaps:

• Safety (timeouts) requires liveness (both parties online)
• If Bob goes offline after Alice claims, Alice gets both assets
• This is not a bug — it's the structural cost of no coordinator
• ShieldedDEX doesn't have this problem (batch coordinator ensures both sides clear)

This is a new dimension in the impossibility space: P2P settlement requires mutual liveness.

DecentralizedCLOB

_{spec · config}

Multiple nodes each maintain independent order books. Orders are submitted to a global pool and delivered to nodes in nondeterministic order — modeling network propagation delay. Each node runs the same price-time priority matching engine as CentralizedCLOB. This models on-chain order books like Serum/OpenBook (Solana, historical), dYdX v4 (Cosmos app-chain where validators run matching), Hyperliquid (L1 with on-chain order book), and Injective (Cosmos chain).

graph LR
    subgraph Global Pool
        OP[Submitted Orders]
    end

    OP -- "order i" --> N1
    OP -- "order j" --> N1
    OP -- "order j" --> N2
    OP -- "order i" --> N2

    subgraph N1["Node 1"]
        direction TB
        BB1[Buy Book] --> ME1{Match}
        SB1[Sell Book] --> ME1
        ME1 --> T1[Trades]
    end

    subgraph N2["Node 2"]
        direction TB
        BB2[Buy Book] --> ME2{Match}
        SB2[Sell Book] --> ME2
        ME2 --> T2[Trades]
    end

    T1 -.- D["Different delivery order<br/>→ different trades"]
    T2 -.- D

The core problem: without consensus on ordering, different nodes process the same orders in different sequences and arrive at different results. TLC proves this is not just a theoretical concern — it finds concrete traces where the same set of orders produces different trades (or no trades at all) at different nodes.

• Per-node matching: same CLOB logic (price-time priority, ask price execution)
• Nondeterministic delivery: any node can receive any unprocessed order next
• Self-trade interaction: delivery order determines which orders get priority, and self-trade prevention can block matches that would succeed in a different sequence

Verified properties (per-node correctness)

Consensus properties (expected to fail)

Add as INVARIANT to see counterexamples:

SandwichAttack

_{spec · config}

Models the canonical MEV (Maximal Extractable Value) attack against a constant-product AMM. An adversary who controls transaction ordering (block builder, sequencer) can extract value from other traders by sandwiching their swaps. This is the primary attack vector against AMMs like Uniswap, and the main motivation behind MEV-resistant designs like Flashbots, Penumbra, and CoW Protocol.

sequenceDiagram
    participant A as Adversary
    participant P as AMM Pool
    participant V as Victim

    Note over P: reserves: 100A / 100B
    V-->>P: pending: swap 10A→B
    Note over A: sees victim's pending tx

    A->>P: 1. Front-run: swap 9A→B
    Note over P: reserves: 109A / 92B<br/>(price of B pushed up)
    P->>A: gets 8B

    V->>P: 2. Victim swap: 10A→B
    Note over P: reserves: 119A / 85B
    P->>V: gets 7B (would have gotten 9B)

    A->>P: 3. Back-run: swap 8B→A
    Note over P: reserves: 109A / 93B
    P->>A: gets 10A

    Note over A: profit: spent 9A, got 10A = +1A
    Note over V: loss: got 7B instead of 9B = -2B

The attack works because AMM pricing is path-dependent: the adversary's front-run changes the reserves, making the victim's swap execute at a worse rate. The adversary then converts back at the new favorable rate.

• Front-run: adversary swaps in the same direction as victim, moving the price
• Victim swap: executes at degraded price due to moved reserves
• Back-run: adversary swaps in the opposite direction, capturing the spread
• Batch auction resistance: OrderingIndependence + UniformClearingPrice make sandwiching impossible in BatchedAuction — there is no price to move between trades

Attack properties (expected to fail)

Add as INVARIANT to see counterexamples:

FrontRunning

_{spec · config}

Models front-running on a CLOB — the CLOB analog of SandwichAttack (which targets AMMs). An adversary who controls transaction ordering consumes cheap sell-side liquidity before a victim's buy order, forcing the victim to fill at worse prices. This models HFT latency arbitrage, block builder front-running, and validator front-running in on-chain CLOBs like dYdX and Serum/OpenBook (historical).

sequenceDiagram
    participant A as Adversary
    participant Book as CLOB Sell Book
    participant V as Victim

    Note over Book: sell 2 units @ 10<br/>sell 3 units @ 15

    V-->>Book: pending: buy 3 units
    Note over A: sees victim's pending order

    A->>Book: 1. Front-run: buy 1 @ 10
    Note over Book: remaining: 1 @ 10, 3 @ 15<br/>(cheap liquidity consumed)

    V->>Book: 2. Victim buys 3 units
    Book->>V: fills: 1 @ 10, 2 @ 15 = 40
    Note over V: would have paid: 2@10 + 1@15 = 35<br/>degradation: +5 (14% worse)

    Note over A: bought 1 unit at 10<br/>market now at ~13.3<br/>profit ≈ 3.3 per unit

Both AMM sandwiching and CLOB front-running exploit ordering power, but through different mechanisms:

• AMM sandwich: adversary shifts the price curve with their own swap
• CLOB front-run: adversary depletes cheap resting orders from the book

Both are structurally impossible in BatchedAuction/ZKDarkPool due to OrderingIndependence.

Verified properties

Attack properties (expected to fail)

Add as INVARIANT to see counterexamples:

LatencyArbitrage

_{spec · config}

Models latency arbitrage between two CLOBs — the core mechanism from Budish, Cramton, and Shim (2015). When a public signal moves the "true" price, one exchange updates faster than the other. A fast trader snipes the stale quote on the slow exchange before the market maker can update. This models the HFT arms race between NYSE and BATS/IEX, cross-exchange crypto arbitrage (Binance vs Coinbase), and cross-L2 latency (Arbitrum vs Optimism).

sequenceDiagram
    participant Fast as Fast Exchange<br/>(updated)
    participant Arb as Arbitrageur
    participant Slow as Slow Exchange<br/>(stale quotes)
    participant MM as Market Maker

    Note over Fast,Slow: both: bid=10, ask=11

    Note over Fast,Slow: PUBLIC SIGNAL: price jumps +3

    Fast->>Fast: updates: bid=13, ask=14
    Note over Slow: still: bid=10, ask=11<br/>(stale!)

    Arb->>Slow: buy 5 units at stale ask=11
    Arb->>Fast: sell 5 units at new bid=13
    Note over Arb: profit: (13-11) × 5 = 10

    Note over MM: lost 10 on stale fills<br/>(adverse selection)

    Slow->>Slow: finally updates: bid=13, ask=14
    Note over Fast,Slow: quotes converged (too late)

Budish et al.'s argument: continuous limit order books create an arms race where speed advantages translate to sniping profits. Batch auctions eliminate this because all orders in a batch get the same price — there is no stale quote to snipe. Our BatchedAuction spec verifies OrderingIndependence, confirming that submission timing cannot affect the clearing price.

• Stale quote sniping: fast trader exploits latency gap between exchanges
• Zero-sum: arbitrageur's profit exactly equals market maker's loss (verified: ZeroSum)
• Quotes converge: after the slow exchange updates, prices are aligned (verified: QuotesConverge)
• Batch auction solution: OrderingIndependence eliminates the concept of "stale" quotes entirely

Verified properties

Latency arbitrage properties (expected to fail)

Add as INVARIANT to see counterexamples:

WashTrading

_{spec · config}

Models wash trading on an AMM: a manipulator trades with themselves (swap A→B then B→A) to inflate reported volume. On a CLOB, self-trade prevention blocks this. On an AMM, there is no counterparty identity — any address can swap. The manipulator loses only fees, but the volume appears genuine on-chain. Estimated 40-70% of DEX volume is wash trading, used to game token listings, airdrops, and liquidity mining rewards.

sequenceDiagram
    participant M as Manipulator
    participant P as AMM Pool

    Note over P: reserves: 100A / 100B

    M->>P: swap 10A → B
    P->>M: gets 9B
    Note over P: reserves: 110A / 91B<br/>volume: 10

    M->>P: swap 9B → A
    P->>M: gets 9A (lost 1A to fees)
    Note over P: reserves: 101A / 100B<br/>volume: 19

    Note over M: started: 30A, 0B<br/>now: 29A, 0B<br/>lost 1A (fees)<br/>but generated 19 units of "volume"

    M->>P: swap 10A → B
    P->>M: gets 9B
    M->>P: swap 9B → A
    P->>M: gets 9A

    Note over M: 2 round-trips:<br/>lost ~3A in fees<br/>generated ~37 in volume<br/>volume/cost ratio ≈ 12x

• No identity check: AMM swaps are permissionless — anyone can trade, no STP
• Round-trip cost: each cycle costs fees (k grows), but cost is small relative to volume generated
• CLOB resistance: NoSelfTrades invariant in CentralizedCLOB prevents wash trading
• Batch auction resistance: NoSelfTrades in BatchedAuction/ZKDarkPool also blocks self-trades

Wash trading properties (expected to fail)

Add as INVARIANT to see counterexamples:

ImpermanentLoss

_{spec · config}

Models the economic risk for liquidity providers (LPs) in a constant-product AMM. An LP deposits tokens into the pool, external traders swap against it (moving the price), and the LP's position is compared to simply holding the original tokens. The difference is impermanent loss (IL) — the LP ends up with fewer tokens (by value) than if they had just held. This is the fundamental risk of providing liquidity on Uniswap, and why protocols offer "liquidity mining" rewards to compensate LPs. See Terminology for definitions.

sequenceDiagram
    participant LP as Liquidity Provider
    participant P as AMM Pool
    participant T as External Trader

    LP->>P: deposit 100A + 100B
    Note over P: reserves: 100A / 100B<br/>k = 10,000

    T->>P: swap 8A → B
    Note over P: reserves: 108A / 93B<br/>k = 10,044 (fees grew k)

    LP->>P: withdraw all
    P->>LP: gets 108A + 93B

    Note over LP: LP has: 108A + 93B<br/>Hold would be: 100A + 100B<br/>At current price (93/108):<br/>LP value = 186.0B<br/>Hold value = 186.1B<br/>IL = 0.1B lost

The loss follows from the AM-GM inequality: any change in the price ratio causes the LP's position to underperform holding, even though fees grow the pool (k increases). The loss is "impermanent" because it disappears if the price returns to the original ratio — the LP keeps the fee income.

• LP deposits: creates the pool with initial reserves
• External swaps: move the price ratio, causing IL
• Fee income: k grows with every swap (0.3% fee), partially compensating IL
• AM-GM inequality: 2 * reserveA * reserveB < InitReserveA * reserveB + InitReserveB * reserveA whenever the price ratio changes

IL property (expected to fail)

Add as INVARIANT to see counterexample:

CrossVenueArbitrage

_{spec · config}

Models arbitrage between a CLOB and an AMM trading the same asset. When prices diverge, an arbitrageur buys on the cheap venue and sells on the expensive one, profiting from the difference. Unlike sandwich attacks, this is "productive" MEV — it aligns prices across venues. But the profit comes at the expense of the AMM LP (impermanent loss). This models the CEX/DEX arbitrage that dominates Ethereum MEV: bots like Wintermute and Jump continuously arbitrage between centralized exchanges and on-chain AMMs.

sequenceDiagram
    participant C as CLOB<br/>(ask = 5B per A)
    participant Arb as Arbitrageur
    participant A as AMM Pool<br/>(price ≈ 10B per A)

    Note over Arb: sees price divergence:<br/>CLOB ask (5) < AMM price (10)

    Arb->>C: buy 1A for 5B
    Arb->>A: swap 1A → B
    A->>Arb: gets 9B
    Note over Arb: profit: 9 - 5 = 4B

    Note over A: reserves: (10,100) → (11,91)<br/>price dropped from 10 to 8.3<br/>LP lost value (IL)

    Arb->>C: buy 1A for 5B
    Arb->>A: swap 1A → B
    A->>Arb: gets 7B
    Note over Arb: profit: 7 - 5 = 2B

    Arb->>C: buy 1A for 5B
    Arb->>A: swap 1A → B
    A->>Arb: gets 6B
    Note over Arb: profit: 6 - 5 = 1B

    Note over A: reserves: (13,78)<br/>price ≈ 6 (converged toward CLOB)<br/>total arb profit: 7B<br/>LP bears the cost

The arbitrageur keeps trading until the AMM price converges to the CLOB range — at which point no more profit is available. TLC verifies that the price always moves in the right direction (PriceNotDiverging holds).

• Atomic trades: arb buys A on CLOB and sells A on AMM in one step (or vice versa)
• Two directions: buy CLOB/sell AMM (when AMM price > CLOB ask) or buy AMM/sell CLOB (when AMM price < CLOB bid)
• Price convergence: each arb trade pushes AMM price toward CLOB range (verified)
• LP cost: arbitrage-driven trades cause impermanent loss for the AMM LP (same AM-GM formula)

Verified properties

Arbitrage properties (expected to fail)

Add as INVARIANT to see counterexamples:

ZKRefinement

_{spec · config}

Formal refinement proof: ZKDarkPool implements BatchedAuction. Adding privacy (sealed bids + order destruction) to a batch auction could, in principle, break correctness — perhaps the commit-reveal protocol changes the clearing outcome, or destroying orders violates conservation. This proof rules that out: it instantiates BatchedAuction with a variable mapping from ZKDarkPool's state, then verifies that all 6 BatchedAuction invariants still hold. This is TLA+'s native method for proving that one specification implements another.

Variable mapping (ZKDarkPool → BatchedAuction)

Verified: all 6 BatchedAuction invariants hold on ZKDarkPool's state space

This confirms that privacy (sealed bids + post-trade order destruction) is a pure addition — it does not alter the clearing mechanism in any way. ZKDarkPool = BatchedAuction + information hiding. This result underpins the claim in conclusions that privacy is a mechanism design tool for MEV elimination: it adds resistance to sandwich attacks and front-running without sacrificing any batch auction guarantee.

Comparison

Same orders, different outcomes — the key structural differences, verified by TLC:

Conclusions

The formal verification reveals a fundamental three-way trade-off between fairness, liquidity, and immediacy. No mechanism dominates — each one guarantees properties the others provably cannot.

What TLC proves (not just argues)

Vulnerability resistance summary (TLC-verified)

ShieldedDEX is the only mechanism that resists all six attack categories. It inherits batch auction resistance to front-running, sandwich, latency arbitrage, spread arbitrage, and wash trading — and adds resistance to asset-targeted attacks because the pair itself is hidden. The cost: cross-pair price discovery is lost.

ShieldedDEX: strongest privacy, least vulnerable clearing

ShieldedDEX combines the strongest privacy guarantees (order contents + asset pair hidden — strictly more than any other mechanism, as shown in the observer visibility table) with the least vulnerable clearing mechanism (batch auction — formally verified to resist front-running, sandwich attacks, spread arbitrage, and latency arbitrage). Its ordering independence makes it safe to decentralize without a sequencer: validators only need consensus on the commitment set, not the sequence, and they never see the contents or target pairs. The cost is immediacy and cross-pair price discovery — structural tradeoffs that no amount of privacy can eliminate.

The impossibility triangle

A mechanism that clears at a uniform price (fairness) must collect orders before clearing, sacrificing immediacy. A mechanism that always has liquidity (AMM) must price algorithmically, creating price impact that depends on ordering. A mechanism that matches immediately (CLOB) exposes different prices to different participants, enabling spread arbitrage. These are structural constraints, not implementation choices — they follow from the definitions of the mechanisms themselves.

Privacy as MEV resistance

The ZKDarkPool spec demonstrates that adding privacy (sealed bids + post-trade order destruction) to a batch auction doesn't change any correctness property — all BatchedAuction invariants carry over — but adds a new dimension: MEV elimination through information hiding. The SandwichResistant invariant proves that the sandwich attack pattern (which succeeds against AMMs in SandwichAttack.tla) is structurally impossible when orders are sealed and cleared at a uniform price. Privacy is not just a feature — it's a mechanism design tool that eliminates the information asymmetry attackers need.

Privacy vs price discovery (the 4th dimension)

The ShieldedDEX spec extends the impossibility triangle into a tetrahedron. Hiding the asset pair in addition to order contents (inspired by Zcash Shielded Assets, ZIP-226/227) eliminates asset-targeted attacks — an attacker cannot even identify which pair to sandwich. But full privacy has a cost: cross-pair arbitrage becomes impossible within the batch because no participant can observe price divergence across pairs. TLC proves this concretely: P1 clears at 1, P2 clears at 2, and no mechanism exists to align them. The tradeoff is not fairness vs liquidity vs immediacy, but fairness vs liquidity vs immediacy vs price discovery — and no mechanism achieves all four.

Centralization vs decentralization

The DecentralizedCLOB spec shows that continuous matching is fundamentally order-dependent — decentralizing it without consensus on transaction ordering leads to divergent state across nodes. This is why real-world decentralized CLOBs (dYdX v4, Hyperliquid) run their own chains with a single sequencer or validator-based consensus to impose a total order. Batched auctions avoid this problem entirely because clearing is order-independent.

Shared Definitions

Common.tla contains reusable definitions across all mechanisms:

• Order tuple accessors: OTrader, OPrice, OQty, OId, OTime
• Trade tuple accessors: TBuyer, TSeller, TPrice, TQty, TTime, TBuyLimit, TSellLimit
• Sequence helpers: RemoveAt, ReplaceAt
• Arithmetic helpers: Min, Max

Terminology

Running the Specs

Requires Java and tla2tools.jar. From the specs/ directory:

java -DTLC -cp /path/to/tla2tools.jar tlc2.TLC <SpecName> -config <SpecName>.cfg -modelcheck

Or use the TLA+ VS Code extension.

References

Real-world systems

Academic

• Budish, Cramton, Shim — "The High-Frequency Trading Arms Race" (2015) — proposes frequent batch auctions to eliminate latency arbitrage