TL;DR
This paper develops formally verified algorithms for double sided auctions with multiple trade quantities, ensuring correctness and enabling automatic violation detection in financial exchanges using proof assistant tools.
Contribution
It extends auction models to multiple quantities, provides formal correctness proofs, and creates verified programs for practical use in market regulation.
Findings
Verified auction algorithms successfully detect violations in real market data.
Formal proofs ensure correctness of auction matching algorithms.
Verified programs can be used by exchanges and regulators for compliance checks.
Abstract
Double sided auctions are widely used in financial markets to match demand and supply. Prior works on double sided auctions have focused primarily on single quantity trade requests. We extend various notions of double sided auctions to incorporate multiple quantity trade requests and provide fully formalized matching algorithms for double sided auctions with their correctness proofs. We establish new uniqueness theorems that enable automatic detection of violations in an exchange program by comparing its output with that of a verified program. All proofs are formalized in the Coq proof assistant without adding any axiom to the system. We extract verified OCaml and Haskell programs that can be used by the exchanges and the regulators of the financial markets. We demonstrate the practical applicability of our work by running the verified program on real market data from an exchange to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
