Description
The design and evaluation of Quartz is grounded in a suite of case study smart contracts. These are intended to span a wide range of application scenarios and design patterns encountered in practice by contract developers. The language’s implementation is organized around the translation of a contract to two targets: a formal specification expressed in TLA+ and an implementation expressed in Solidity. Through its support for model checking contract specifications, Quartz enables the discovery of implementation flaws identical to those that have compromised real-world smart contracts. Moreover, its generated Solidity code imposes at most minor execution overhead compared to equivalent handwritten code. Finally, we discuss Quartz’s future potential to validate contracts against economic notions, of correctness, which are often central concerns in contract design yet are not addressed by current verification techniques.