spot-clob

Fully onchain spot CLOB on Monad — Foundry/Solidity scaffold.

A Foundry implementation of a fully onchain spot central limit order book: a Vault singleton for custody and internal balances, a permissionless Factory that deploys one immutable Market per token pair, and the Market order book itself (tick levels, FIFO price-time priority, escrow-locked resting orders, a fixed 3 bps taker fee).

Contracts (src/)

Contract	Responsibility
Vault	Custody + internal balances. Measure-received deposits; withdraw is always open. Escrow lock/unlock/settle moves are callable only by factory-registered markets.
Factory	Permissionless CREATE2 market creation. Identity tuple (base, quote, tickSize, lotSize) is the salt; duplicates revert. Registers each market with the vault.
Market	One immutable book per pair. Limit / post-only / IOC / market orders, continuous price-time matching, taker-pays gas bounded by maxSlots.
libraries/HierBitmap	Three-level hierarchical tick bitmap over the [0, 2^24) range for best-price discovery.
libraries/TickMath	Geometric tick↔price grid: price(tick) = 1.0001^(tick - OFFSET) in Q128.128 (Uniswap v3-style). Proven strictly monotone / bounded-error / in-range by the Price Lemma.
libraries/BitMath	Least/most-significant-bit helpers.

Pricing

Orders are denominated in base amount (with lotSize the minimum) and priced on a geometric tick grid — price(tick) = 1.0001^(tick − OFFSET) (constant relative granularity across price magnitudes, so a market's price level need not be known at creation). tickSize is the tick spacing; OFFSET = 2^23 is price 1.0. Price is Q128.128 (priceX128); the quote for an amount is amount · price / 2^128, rounded up for what a buy-taker pays and for what a bid escrows, so every rounding favors the vault (I7). The concrete priceX128 routine is proven strictly monotone, bounded-error (≤ 2⁻⁴⁰) and range-safe over the whole ±600000 tick domain by the Price Lemma, which discharges the monotone-price ghost the Market CVL spec assumes.

Storage is laid out for MIP-8 (Monad's page-aware gas accounting): each price level embeds its FIFO queue in one contiguous region, levels live in a fixed-size array (no keccak-derived slots anywhere in Market), and each level's stride is padded to a whole 128-slot page so every level starts page-aligned.

Tests (test/)

Unit + fuzz tests per contract (Vault.t.sol, Factory.t.sol, Market.t.sol, HierBitmap.t.sol, TickMath.t.sol — the last pins the geometric curve to high-precision reference values) plus a stateful invariant suite (invariant/) asserting the core invariants — I1 solvency, I2 conservation, I5 cancellation safety, I6 withdrawal liveness — over randomized deposit/order/cancel/withdraw sequences.

Formal verification (Certora)

certora/ holds the CVL specification: 55 rules across nine spec files — the Vault (I1 solvency, I5/I6, and the G1–G4 interface guarantees), the SafeERC20 boundary against non-standard tokens, the Market (I2/I3/I4/I5-book/I7 and the book-structure invariants, in a sound front that summarizes the match loop by a proven model and needs no unrolling flags, plus a bounded front against the real loop), the inductive step lemmas for both match loops that discharge that model, the HierBitmap library as an abstract set, and the BS5 bit⟺liveness coupling. Every rule is discharged on every PR by the open-source Certora Prover, entirely locally — no CERTORAKEY, no cloud (.github/workflows/certora.yml). The Market spec's monotone-price ghost is discharged separately by the Price Lemma — proof-by-exhaustion over all ~1.2M ticks, cross-checked bit-for-bit against the compiled bytecode. Each proven rule is paired with a planted bug in certora/mutations/ that must turn it red. Architecture, scoping decisions, and the exact trust boundaries are in certora/README.md.

Prerequisites

• Foundry (forge, cast, anvil)

Install with:

curl -L https://foundry.paradigm.xyz | bash
foundryup

Getting started

Clone the repo and install dependencies with Foundry:

git clone https://github.com/monad-exp/spot-clob
cd spot-clob
forge install foundry-rs/forge-std

forge install fetches forge-std into lib/. Run it once after cloning (and to add further dependencies later).

Usage

Build

forge build

Test

forge test

Format

forge fmt

Gas snapshots

forge snapshot

Deploy

Set the target RPC (and a funded deployer key) as environment variables, then run the script:

export MONAD_TESTNET_RPC_URL="https://testnet-rpc.monad.xyz"
# DeployScript deploys Vault + Factory and wires them together.
forge script script/Deploy.s.sol:DeployScript \
  --rpc-url monad_testnet \
  --private-key $PRIVATE_KEY \
  --broadcast

Monad network references:

Network	Chain ID	RPC env var
Monad testnet	10143	MONAD_TESTNET_RPC_URL
Monad mainnet	—	MONAD_MAINNET_RPC_URL

Layout

src/      — contracts
test/     — tests
script/   — deployment / operational scripts
lib/      — dependencies (installed via `forge install`)

CI

GitHub Actions runs on every push to main and on pull requests:

• forge fmt --check, forge build, forge test (test.yml),
• the full Certora suite, locally with the open-source prover (certora.yml),
• the Price Lemma, when the price routine or compiler settings change (price-lemma.yml).