# ClassInvGen: Class Invariant Synthesis using Large Language Models

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 50 references that are in the map.
- First posted on arXiv 26 Feb 2025.

## Builds on (most cited first, 14 of 14)

- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [Retrieval-Augmented Generation for Large Language Models: A Survey](https://mlsanity.com/paper/2312.10997/) (2023)
- [An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation](https://mlsanity.com/paper/2302.06527/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models](https://mlsanity.com/paper/2310.15991/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic](https://mlsanity.com/paper/1903.09713/) (2019)
- [Fuzzing Class Specifications](https://mlsanity.com/paper/2201.10874/) (2022)
- [Are My Invariants Valid? A Learning Approach](https://mlsanity.com/paper/1903.06089/) (2019)
- [Using human-in-the-loop synthesis to author functional reactive programs](https://mlsanity.com/paper/1909.11206/) (2019)

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

- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems](https://mlsanity.com/paper/2511.14435/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [A Blueprint for AI-Driven Software Quality: Integrating LLMs with Established Standards](https://mlsanity.com/paper/2505.13766/) (2025)
- [Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs](https://mlsanity.com/paper/2603.15510/) (2026)
- [Agentic Separation Logic Specification Synthesis](https://mlsanity.com/paper/2605.27531/) (2026)
- [AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis](https://mlsanity.com/paper/2606.20969/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [Multi-Large Language Model Orchestrated Severity Assessment of Clinical Records (MOSAIC)](https://mlsanity.com/paper/2607.05032/) (2026)
- [Self-Spec Verifiable Code Generation](https://mlsanity.com/paper/2609.39568/) (2026)

## Abstract (arXiv)

Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants. In this work, we describe ClassInvGen, a method for co-generating executable class invariants and test inputs to produce high-quality class invariants for a mainstream language such as C++, leveraging LLMs' ability to synthesize pure functions. We show that ClassInvGen outperforms a pure LLM-based technique to generate specifications (from code) as well as prior data-driven invariant inference techniques such as Daikon. We contribute a benchmark of standard C++ data structures along with a harness that can help measure both the correctness and completeness of generated specifications using tests and mutants. We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++ codebase.