Formal Tools for Specifying Financial Smart Contracts

Abstract

Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. Because of this, much work has been done in formal verification of smart contracts to prove a contract correct with regards to its specification. However, financial smart contracts have complicated specifications, and it is not all straightforward to write one which correctly describes its intended behaviors. As a response to this challenge, we develop formal tools for specifying financial smart contracts. We target aspects of contract specification which are typically difficult to address and which can be a source of expensive contract vulnerabilities. In doing so, we hope to expand the capability of formal methods to specify desired contract behavior and thereby prevent catastrophic loss of funds.