UC Berkeley

Blockchain-based smart contracts have emerged as a popular means of enforcing agreements among a collection of parties without a prior assumption of trust. However, it has proven difficult to write correct contracts that are robust when operating in the adversarial environment of public blockchains. This thesis evaluates the ability of a domain-specific contract programming language to support the expression and systematic testing of practical smart contracts. We present the design, implementation, and evaluation of Quartz, a contract language based on the state machine model of execution.

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.