一句话：提出 SmartSpec，从功能与安全规约出发，结合演绎与归纳合成最大许可的智能合约实现并集成验证。
智能合约管理区块链上的大量数字资产，其透明性与不可篡改性要求在部署前保证正确性，但现有验证工具的迭代流程对经验不足的开发者并不友好。本文提出一种开发范式的转变：不再书写底层代码，而是编写高层规约。为此作者设计了 SmartSpec，一个从功能规约与安全规约自动生成合约实现的合成器，并借助集成验证对结果进行校验。为避免生成过于受限的合约，SmartSpec 采用最大许可（maximally permissive）合成策略，在保留全部安全需求的前提下尽可能放宽行为，其算法融合演绎合成与归纳合成，以在精确性与泛化能力之间取得平衡。作者在 27 个合约上进行了评估：合成在数秒至数分钟内完成，其中 23 个无需交互式精化即与参考实现一致（85%），其余 4 个可通过额外示例进行最多四轮交互反馈后修正；在榜合约相对参考实现的平均 gas 开销为 +0.7%。
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%.