CentralizedCLOB
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
| Property | Type | Description |
|---|---|---|
| PositiveBookQuantities | Invariant | Every resting order has quantity > 0 |
| PositiveTradeQuantities | Invariant | Every trade has quantity > 0 |
| PriceImprovement | Invariant | Trade price <= buyer's limit and >= seller's limit |
| NoSelfTrades | Invariant | No trade has the same buyer and seller |
| UniqueOrderIds | Invariant | All order IDs on the books are distinct |
| ConservationOfAssets | Invariant | Trade log is consistent across traders |
| EventualMatching | Liveness | Crossed books between different traders are eventually resolved |
Comparison properties (expected to fail)
Add as INVARIANT in CentralizedCLOB.cfg to see a counterexample:
| Property | Description |
|---|---|
| AllTradesSamePrice | All trades execute at the same price (FAILS: CLOB trades execute at the resting order's price, which varies — this is what enables spread arbitrage. Contrast with BatchedAuction where UniformClearingPrice holds by construction) |