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 workflow for the automatic construction of finite-state machines implementing the control flow of a smart contract. As specification language, we use temporal stream logic (TSL), which builds on LTL but adds additional mechanisms to reason about the control flow of infinite data. Our specifications not only reason about the order of transactions based on guards like access rights, but also include the updates of fields necessary for a correct control flow. We show how to comprehensively specify the control flow of various types of common smart contracts, including auctions, asset transfers, and crowd funding protocols. Our tool \tool implements the approach using BDD-based symbolic algorithms, resulting in a fast reactive control flow synthesis.