  We use formal methods to specify, design, and monitor continuous double
auctions, which are widely used to match buyers and sellers at exchanges of
foreign currencies, stocks, and commodities. We identify three natural
properties of such auctions and formally prove that these properties completely
determine the input-output relationship. We then formally verify that a natural
algorithm satisfies these properties. All definitions, theorems, and proofs are
formalized in an interactive theorem prover. We extract a verified program of
our algorithm to build an automated checker that is guaranteed to detect errors
in the trade logs of exchanges if they generate transactions that violate any
of the natural properties.
