# Formal verification of trading in financial markets

## TL;DR

This paper develops a formal framework using the Coq proof assistant to verify fairness, uniformity, and individual rationality in algorithmic trading matchings at financial exchanges.

## Contribution

It introduces a formal, axiomatic approach to verify regulatory properties of trading algorithms in financial markets using theorem proving.

## Key findings

- Formal definitions of fairness, uniformity, and individual rationality.
- Formal proofs of properties for specific auction classes.
- Complete formalization in Coq without additional axioms.

## Abstract

We introduce a formal framework for analyzing trades in financial markets. An exchange is where multiple buyers and sellers participate to trade. These days, all big exchanges use computer algorithms that implement double sided auctions 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 \emph{fair}, \emph{uniform} and \emph{individual rational}. To verify these properties of trades, we first formally define these notions in a theorem prover and then give formal proofs of relevant results on matchings. Finally, we use this framework to verify properties of two important classes of double sided auctions. All the definitions and results presented in this paper are completely formalised in the Coq proof assistant without adding any additional axioms to it.