Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models

We present a framework that leverages large language models (LLMs) to guide the synthesis of inductive invariants for distributed systems. The approach iteratively queries an LLM to propose candidate predicates, integrates them into decision-tree learners, and refines the search using counterexample feedback from a model checker. Experiments on classic leader-election, mutual-exclusion, and consensus protocols show that our method discovers tight invariants with up to a 4× reduction in synthesis iterations compared with purely heuristic template-based baselines.

In Formal Methods in Computer-Aided Design (FMCAD 2025) — accepted, to appear