The Design and Regulation of Exchanges: A Formal Approach

TL;DR

This paper employs formal methods to specify, verify, and automate the regulation of continuous double auctions, ensuring they meet natural properties and detecting errors in exchange trade logs.

Contribution

It introduces a formal framework for designing and verifying exchange algorithms, including an automated checker for error detection in trade logs.

Findings

Formal properties fully characterize auction input-output behavior

Verified algorithm satisfies the specified properties

Automated checker detects violations in trade logs

Abstract

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.