Precise Invariant Generation via Interleaved Agentic Reasoning and Program Analysis

Programmers increasingly rely on Large Language Models (LLMs) to generate code, yet nothing guarantees the code they generate is correct. Recent work has attempted to mitigate this issue by leveraging formal verification tools to certify that LLM-written code is correct. However, existing verifiers cannot scale to real-world software unless they are provided with invariants to guide the verification process. Generating correct and useful invariants is a long-standing unsolved problem: existing formal methods approaches cannot handle larger programs, while LLM-based approaches struggle to reason about the low-level semantics necessary to generate precise invariants. We present a novel approach to invariant generation that achieves the best of both worlds, interleaving LLM-based invariant generation with structured formal analyses. Our strategy first uses program transformations to reduce the input program and tailor its structure for LLM-based reasoning. It then runs a medley of existing and novel analyses on the input program to construct a formal knowledge base of program analysis information. The combination of the reduced program with the formal knowledge base enables an invariant generation agent to produce invariants that are correct and precise enough for program verification. We implement this approach in a tool (STRIVE). STRIVE solves up to $3.9\times$ as many problems as existing LLM-based approaches and up to $5.7\times$ as many as solver-based approaches.