交易所的设计与监管：一种形式化方法

我们使用形式化方法来规范、设计和监控连续双向拍卖，这种拍卖机制被广泛用于在外汇、股票和商品交易所中匹配买卖双方。我们识别了此类拍卖的三个自然属性，并形式化证明了这些属性完全决定了输入-输出关系。随后，我们形式化验证了一个自然算法满足这些属性。所有的定义、定理和证明均在交互式定理证明器中形式化。我们提取了算法的已验证程序，以构建一个自动化检查器，如果交易所生成的交易违反了任何自然属性，该检查器保证能检测到交易日志中的错误。