We present a novel and efficient method for synthesis of parameterized distributed protocols by sketching. Our method is both syntax-guided and counterexample-guided, and utilizes a fast equivalence reduction technique that enables efficient completion of protocol sketches, often significantly reducing the search space of candidate completions by several orders of magnitude. To our knowledge, our tool, Scythe, is the first synthesis tool for the widely used specification language TLA+. We evaluate Scythe on a diverse benchmark of distributed protocols, demonstrating the ability to synthesize a large scale distributed Raft-based dynamic reconfiguration protocol beyond the scale of what existing synthesis techniques can handle.

翻译：我们提出了一种新颖且高效的方法，用于通过草图综合参数化分布式协议。该方法同时采用语法引导和反例引导策略，并利用一种快速的等价约简技术，能够高效地完成协议草图的填充，通常将候选完成的搜索空间降低数个数量级。据我们所知，我们的工具Scythe是首个面向广泛使用的规范语言TLA+的综合工具。我们在多样化的分布式协议基准上对Scythe进行了评估，展示了其综合大规模基于Raft的动态重配置协议的能力，其规模超越了现有综合技术所能处理的范围。