# SpecGen: Automated Generation of Formal Program Specifications via Large Language Models

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

## Key facts

- Cited by 53 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jan 2024.

## Built on by (most cited first, 30 of 53)

- [Large Language Model-Based Agents for Software Engineering: A Survey](https://mlsanity.com/paper/2409.02977/) (2024)
- [From LLMs to LLM-based Agents for Software Engineering: A Survey of Current, Challenges and Future](https://mlsanity.com/paper/2408.02479/) (2024)
- [SpecRover: Code Intent Extraction via LLMs](https://mlsanity.com/paper/2408.02232/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [LLM-Based Agentic Systems for Software Engineering: Challenges and Opportunities](https://mlsanity.com/paper/2601.09822/) (2026)
- [Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving](https://mlsanity.com/paper/2512.23511/) (2025)
- [Specification-Based Code-Text-Code Reengineering for LLM-Mediated Software Evolution](https://mlsanity.com/paper/2605.25232/) (2026)
- [EditLord: Learning Code Transformation Rules for Code Editing](https://mlsanity.com/paper/2504.15284/) (2025)
- [Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision](https://mlsanity.com/paper/2508.18675/) (2025)
- [FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight](https://mlsanity.com/paper/2602.11136/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs](https://mlsanity.com/paper/2502.15217/) (2025)
- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [Evaluating Program Semantics Reasoning with Type Inference in System F](https://mlsanity.com/paper/2509.23686/) (2025)
- [Large Language Models for Software Testing: A Research Roadmap](https://mlsanity.com/paper/2509.25043/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [Goal2Story: A Multi-Agent Fleet based on Privately Enabled sLLMs for Impacting Mapping on Requirements Elicitation](https://mlsanity.com/paper/2503.13279/) (2025)
- [Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning](https://mlsanity.com/paper/2509.06239/) (2025)
- [TREAT: A Code LLMs Trustworthiness / Reliability Evaluation and Testing Framework](https://mlsanity.com/paper/2510.17163/) (2025)
- [ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair](https://mlsanity.com/paper/2602.12058/) (2026)
- [Can LLM Aid in Solving Constraints with Inductive Definitions?](https://mlsanity.com/paper/2603.03668/) (2026)

## Abstract (arXiv)

Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. It is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models. Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM to generate appropriate specifications for a given program. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing purely LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.