Efficient and Verified Continuous Double Auctions

ArXiv ID: 2412.08624 “View on arXiv”

Authors: Unknown

Abstract

Continuous double auctions are commonly used to match orders at currency, stock, and commodities exchanges. A verified implementation of continuous double auctions is a useful tool for market regulators as they give rise to automated checkers that are guaranteed to detect errors in the trade logs of an existing exchange if they contain trades that violate the matching rules. We provide an efficient and formally verified implementation of continuous double auctions that takes $O(n \log n)$ time to match $n$ orders. This improves an earlier $O(n^2)$ verified implementation. We also prove a matching $Ω(n\log n)$ lower bound on the running time for continuous double auctions. Our new implementation takes only a couple of minutes to run on ten million randomly generated orders as opposed to a few days taken by the earlier implementation. Our new implementation gives rise to an efficient automatic checker. We use the Coq proof assistant for verifying our implementation and extracting a verified OCaml program. While using Coq’s standard library implementation of red-black trees to obtain our improvement, we observed that its specification has serious gaps, which we fill in this work; this might be of independent interest.

Keywords: Continuous Double Auction, Formal Verification, Order Matching, Red-Black Trees, Time Complexity, Multi-Asset

Complexity vs Empirical Score

• Math Complexity: 6.5/10
• Empirical Rigor: 4.0/10
• Quadrant: Lab Rats
• Why: The paper involves significant theoretical computer science, including formal proofs of algorithmic lower bounds and verification of correctness using Coq, which is mathematically dense. However, the empirical validation is limited to runtime comparisons on synthetic data and lacks real-world backtests or statistical metrics on market data.

  flowchart TD
    Goal["Research Goal<br/>Efficient & Verified Continuous Double Auction Implementation"]
    Inputs["Data/Inputs<br/>- Millions of Random Orders<br/>- Trade Logs from Exchanges"]
    Method["Methodology<br/>- Formal Verification (Coq Proof Assistant)<br/>- O(n log n) Algorithm using Red-Black Trees<br/>- Improved Standard Library Specifications"]
    Process["Computational Process<br/>- Automated Order Matching<br/>- Extraction to OCaml Program"]
    Outcomes["Key Findings & Outcomes<br/>- Lower Bound: Ω(n log n)<br/>- Verified Implementation (Minutes vs Days)<br/>- Efficient Automatic Error Checker"]

    Goal --> Inputs
    Inputs --> Method
    Method --> Process
    Process --> Outcomes