# Efficient Synthesis of Symbolic Distributed Protocols by Sketching

arXiv: https://arxiv.org/abs/2405.07807 · HTML: https://mlsanity.com/paper/2405.07807/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 May 2024.

## Built on by (most cited first, 1 of 1)

- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)

## Abstract (arXiv)

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.