[Paper] Learning Provably Correct Distributed Protocols Without Human Knowledge

Source: arXiv - 2601.22369v1

Overview

Designing distributed protocols that are provably correct—guaranteeing safety and liveness despite message loss, crashes, or malicious actors—has traditionally been a painstaking, expert‑only effort. The new paper presents GGMS, a learning‑based framework that can automatically synthesize such protocols from scratch, without any human‑provided design knowledge. By marrying game‑theoretic search, transformer‑style encoding, and formal model‑checking feedback, the authors push the frontier of automated protocol synthesis to settings that were previously out of reach.

Key Contributions

• Formulation as an imperfect‑information game: Protocol synthesis is cast as searching for a winning strategy in a multi‑agent game where each participant only sees a partial view of the system state.
• GGMS learning pipeline: Introduces a hybrid search architecture that combines:
  1. Monte Carlo Tree Search (MCTS) with a custom action encoder built on transformers to efficiently explore huge strategy spaces.
  2. Global depth‑first search (DFS) to escape local minima that MCTS alone can get stuck in.
  3. Iterative model‑checking feedback that prunes invalid strategies and guides the search toward provably correct ones.
• Theoretical guarantee: Proves search completeness under mild assumptions—if a correct protocol exists within the bounded model, GGMS will eventually discover it.
• Empirical scaling: Demonstrates synthesis of correct protocols for larger numbers of agents and more complex failure models than prior automated approaches could handle.

Methodology

1. Problem Encoding

   • The distributed system is modeled as a game where each node (agent) selects actions based on its local observations.
   • Desired correctness properties (e.g., consensus, fault‑tolerance) are expressed in SMT (Satisfiability Modulo Theories) formulas, enabling precise, machine‑readable specifications.

2. Search Engine (GGMS)

   • Monte Carlo Tree Search builds a search tree of partial strategies. At each node, a transformer‑based action encoder predicts promising actions by learning patterns from previously explored strategies.
   • When MCTS converges to a local optimum (no further improvement), a global DFS is launched to systematically explore alternative branches that might have been overlooked.
   • After each candidate protocol is generated, a model checker exhaustively verifies it against the SMT specifications. Counterexamples are fed back to the search, shaping future exploration.

3. Iterative Refinement Loop

   • The cycle of proposal → verification → feedback repeats until a protocol passes the model checker (i.e., is provably correct) or the search space is exhausted.

Results & Findings

• Success Rate: GGMS solved all benchmark instances where earlier tools either timed out or returned incomplete solutions.
• Search Efficiency: The transformer‑guided MCTS reduced the number of explored states by up to 70 % compared to vanilla MCTS.
• Verification Overhead: Model‑checking each candidate added modest runtime (seconds to minutes) but dramatically improved convergence, acting as a strong pruning signal.

Practical Implications

• Rapid Prototyping of Fault‑Tolerant Services: Engineers can feed high‑level safety/liveness specs (e.g., “all replicas must eventually agree”) and obtain a correct-by-construction protocol, cutting weeks of manual design.
• Custom Consensus for Edge/IoT: Resource‑constrained environments often need lightweight consensus algorithms tuned to specific failure patterns. GGMS can synthesize bespoke protocols that are formally verified, reducing reliance on heavyweight off‑the‑shelf solutions.
• Security Auditing: By automatically generating all correct strategies within a bounded model, developers gain a concrete artifact to audit, test, and compare against hand‑crafted implementations.
• Educational Tooling: The framework can serve as a teaching aid, letting students experiment with protocol design and instantly see formal correctness feedback.

Limitations & Future Work

• Bounded Model Assumption: Correctness is guaranteed only within the finite horizon and state space explored during synthesis; extending to unbounded or infinite‑state systems remains open.
• Scalability Ceiling: While GGMS scales better than prior methods, the combinatorial explosion still limits practical synthesis to roughly a dozen agents in the current implementation.
• Specification Burden: Translating complex real‑world requirements into SMT formulas can be non‑trivial for practitioners unfamiliar with formal methods.
• Future Directions: The authors suggest integrating abstraction techniques to handle larger systems, exploring reinforcement learning for richer policy representations, and building higher‑level DSLs (domain‑specific languages) to simplify specification authoring.

Authors

• Yujie Hui
• Xiaoyi Lu
• Andrew Perrault
• Yang Wang

Paper Information

• arXiv ID: 2601.22369v1
• Categories: cs.AI, cs.DC
• Published: January 29, 2026
• PDF: Download PDF