Formally Verified Trades in Financial Markets
Suneel Sarswat, Abhishek Kr Singh

TL;DR
This paper presents a formal framework using the Coq proof assistant to verify fairness, uniformity, and rationality in financial market trades, ensuring compliance with regulatory guidelines.
Contribution
It introduces a formalized approach to verify key properties of trading mechanisms in financial markets using theorem proving.
Findings
Formal definitions of fairness, uniformity, and individual rationality in trades.
Verification of properties for two classes of double-sided auction mechanisms.
Complete formalization in Coq without additional axioms.
Abstract
We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be fair, uniform and individual rational. To verify these properties of trades, we first formally define these notions in a theorem prover and then develop many important results about matching demand and supply. Finally, we use this framework to verify properties of two important classes of double sided auction mechanisms. All the definitions and results presented in this paper are completely formalized in the Coq proof assistant without adding any additional axioms to it.
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
