What does this research mean for the field?

Integrating Large Language Models as predicate prompters within a revision framework significantly improves the synthesis of high-quality program invariants for distributed systems compared to direct LLM generation, achieving performance comparable to state-of-the-art symbolic methods. Novelty: ClaimNovelty.METHODOLOGICAL. Consensus alignment: ConsensusAlignment.NEUTRAL.

What question did this study set out to answer?

The aim is to enhance the synthesis of program invariants using large language models (LLMs) and investigate their efficacy in verification tasks.

June 21, 2026Open Access

Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models

Key Points

The aim is to enhance the synthesis of program invariants using large language models (LLMs) and investigate their efficacy in verification tasks.
Developed two frameworks, PSyn and ISyn, for LLM-assisted invariant synthesis.
Tested methods on 8 distributed systems modeled in Promela.
Used Spin for verifying the synthesized invariants.
GPT-o3 generated invariants directly was less effective than the symbolic invariant synthesis method RunVS.
The integrated approach PSyn significantly outperformed GPT-o3 and ISyn.
PSyn produced higher-quality invariants comparable to RunVS.

Abstract

Deductive verifcation is an approach where the user expends effort in constructing a program invariant manually, or learns this invariant from program traces, and subsequently uses the program invariant for safety verifcation tasks.Most existing invariant synthesis tools still rely on model checking methods to certify invariants, use enumerative search to identify and refne candidate invariants, and user insights to start with a set of candidate predicates that may appear in the fnal (learned) invariant.On the other hand, pre-trained large language models (LLMs) have recently attracted considerable attention in various tasks related to generating program code (e.g., from natural language).There have been recent efforts at applying LLMs to the program verifcation context.In this paper, we investigate the capabilities of LLMs to synthesize program invariants by creating a specialized set of prompts.When LLM invariant synthesis with direct prompting fails, we introduce two revision frameworks for incorporating LLM calls.In the frst framework PSyn, the LLM suggests atomic predicates based on counterexamples for reconstructing the invariants.The second framework ISyn adopts the LLM to generate invariants by itself within a revision process.We tested our methods on 8 distributed systems modeled in Promela and invariants are verifed with Spin.Our results show that the state-of-the-art model GPT-o3, when it is used to generate invariants directly, is less effective than the symbolic invariant synthesis method RunVS.However, our integrated approach PSyn, which employs the LLM as a predicate prompter, signifcantly outperforms GPT-o3 and ISyn and has comparable performance with RunVS.This integrated technique also produces higher-quality invariants in general.Because we focus on runtime monitoring frameworks, we primarily consider system traces and hence likely invariants.However, our revision frameworks can also learn true invariants by using model checkers in the revision frameworks.

Bookmark

View Full Paper