  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 automatically check for
violations in the exchange algorithm.
