Formal Market Mechanisms

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.

Read the full book · Read the blog post

Key results (all TLC-verified, not just argued)

• An impossibility triangle between fairness, liquidity, and immediacy — no mechanism can provide all three
• Batch auctions are safe to decentralize (OrderingIndependence); CLOBs are not (TLC counterexample: same orders → different trades at different nodes)
• Sandwich attacks, front-running (ordering), and latency arbitrage are structurally impossible in batch auctions — formally verified, not just claimed; ZKDarkPool extends this to information-based front-running via sealed bids
• Privacy (sealed bids + order destruction) is a mechanism design tool for MEV elimination, proven equivalent to batch clearing via refinement mapping
• Asset-type privacy (ShieldedDEX) adds a 4th dimension to the impossibility triangle — privacy vs price discovery — but does NOT fix the original three-way tradeoff
• AMMs provide always-available liquidity but are vulnerable to sandwich attacks, wash trading, and impermanent loss — all with TLC counterexamples
• ShieldedDEX is the only mechanism to resist all 6 attack categories (6/6) — combining the strongest privacy with the least vulnerable clearing mechanism
• ShieldedAtomicSwap enables fully P2P cross-chain settlement with unlinkability — observer cannot connect the two legs of a swap (no coordinator, no mempool, no hash linkage)

Specs

Mechanisms

Spec	Description
CentralizedCLOB	Continuous limit order book with price-time priority matching
BatchedAuction	Periodic auction clearing at uniform price that maximizes volume
AMM	Constant-product market maker (x*y=k)
ZKDarkPool	Sealed-bid batch auction with commit-reveal protocol
ShieldedDEX	Multi-asset shielded exchange — asset pair hidden in commitment (novel)
ShieldedAtomicSwap	P2P cross-chain settlement with unlinkability — no coordinator (novel)
DecentralizedCLOB	Multi-node CLOB with nondeterministic order delivery

Attacks & Economic Properties

Spec	Description
SandwichAttack	AMM sandwich attack (front-run + back-run)
FrontRunning	CLOB front-running via liquidity depletion
LatencyArbitrage	Cross-exchange stale quote sniping (Budish et al. 2015)
WashTrading	AMM volume inflation via self-trading round-trips
ImpermanentLoss	LP economic risk from price movement
CrossVenueArbitrage	CLOB-AMM price convergence arbitrage

Proofs

Spec	Description
ZKRefinement	Formal proof: ZKDarkPool implements BatchedAuction

Shared

Spec	Description
Common	Order/trade accessors, sequence helpers, arithmetic utilities

Vulnerability resistance (TLC-verified)

Attack	CLOB	Decentralized CLOB	Batch Auction	ZKDarkPool	ShieldedDEX	AMM
Front-running	Vulnerable	Vulnerable	Resistant (ordering only)	Resistant	Resistant	N/A
Sandwich	Trust assumption	Vulnerable	Resistant	Resistant	Resistant	Vulnerable
Latency arbitrage	Vulnerable	Vulnerable	Resistant	Resistant	Resistant	N/A
Wash trading	Resistant	Resistant	Resistant	Resistant	Resistant	Vulnerable
Spread arbitrage	Vulnerable	Vulnerable	Resistant	Resistant	Resistant	Vulnerable
Asset-targeted	Vulnerable	Vulnerable	Vulnerable	Vulnerable	Resistant	Vulnerable
Score	1/6	1/6	4/6	5/6	6/6	1/6

Running

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

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

See Running the Specs for the full list of commands, or use the TLA+ VS Code extension.

References

Mechanism	Real-world systems
CentralizedCLOB	NYSE, NASDAQ, CME, Binance, Coinbase
BatchedAuction	Penumbra, CoW Protocol, NYSE/NASDAQ opening & closing auctions
AMM	Uniswap v2, SushiSwap, PancakeSwap, Curve, Balancer
ZKDarkPool	Penumbra, Renegade, MEV Blocker
ShieldedDEX	Zcash ZSA (ZIP-226/227), Penumbra, Anoma
ShieldedAtomicSwap	Zcash ZSA (ZIP-226/227), Komodo AtomicDEX, ZK-contingent payments
DecentralizedCLOB	Serum/OpenBook, dYdX v4, Hyperliquid

Academic: Budish, Cramton, Shim — "The High-Frequency Trading Arms Race" (2015)