Reactive Synthesis of Smart Contract Control Flows

Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of state machines implementing the temporal control flow of smart contracts. To accommodate typical smart contract specifications, we build on temporal stream logic (TSL) and extend it with a tailored form of parameterization. We show how to comprehensively specify the control flow of various types of common smart contracts, including ERC20 token systems, elections, and asset transfer protocols. We develop a synthesis algorithm based on the past-time fragment of TSL with parameters and show how to efficiently translate the resulting infinite-state machine to Solidity code. Our tool SCSynt implements the approach together with a feedback loop that warns the developer of potential specification errors. Our experiments show that SCSynt derives correct-by-construction Solidity code from formal smart contract specifications within seconds.