Smart Contract Synthesis via Multi-modal Specifications

Abstract

Smart contracts manage substantial digital assets on blockchains. Given their transparency and immutability, ensuring their correctness before deployment is essential. While verification tools offer assistance, the iterative nature of the process presents hurdles, especially for less experienced developers. In this paper, we explore a paradigm shift in smart contract development: writing high-level specifications instead of low-level code. To realize this goal, we propose SmartSpec, a synthesizer that generates smart-contract implementations from functional and safety specifications and validates them with integrated verification. To avoid overly restrictive outcomes, SmartSpec employs maximally permissive synthesis, ensuring contracts preserve all safety requirements while remaining as permissive as possible. Its novel algorithm combines deductive and inductive synthesis techniques, balancing precision and generalization. On 27 contracts, synthesis runs in seconds to minutes; 23 match references without interactive refinement (85%), while the remaining four can be corrected with up to four rounds of interactive feedback through extra examples. Mean gas overhead vs. references on the table is +0.7%.