# Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification

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

## Key facts

- Cited by 58 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Mar 2024.

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

- [Large Language Model-Based Agents for Software Engineering: A Survey](https://mlsanity.com/paper/2409.02977/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [Validating Network Protocol Parsers with Traceable RFC Document Interpretation](https://mlsanity.com/paper/2504.18050/) (2025)
- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification](https://mlsanity.com/paper/2509.23061/) (2025)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision](https://mlsanity.com/paper/2508.18675/) (2025)
- [Towards Repository-Level Program Verification with Large Language Models](https://mlsanity.com/paper/2509.25197/) (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)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [Integrating Expert Knowledge into Logical Programs via LLMs](https://mlsanity.com/paper/2502.12275/) (2025)
- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [textttReMind: Understanding Deductive Code Reasoning in LLMs](https://mlsanity.com/paper/2511.00488/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Automated Lemma Discovery in Agentic Program Verification](https://mlsanity.com/paper/2603.22114/) (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)
- [Optimizing Code Runtime Performance through Context-Aware Retrieval-Augmented Generation](https://mlsanity.com/paper/2501.16692/) (2025)

## Abstract (arXiv)

Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof relies on domain expertise and non-trivial manpower. In view of such needs, an automated approach for specification synthesis is desired. While existing automated approaches are limited in their versatility, i.e., they either focus only on synthesizing loop invariants for numerical programs, or are tailored for specific types of programs or invariants. Programs involving multiple complicated data types (e.g., arrays, pointers) and code structures (e.g., nested loops, function calls) are often beyond their capabilities. To help bridge this gap, we present AutoSpec, an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It is driven by static analysis and program verification, and is empowered by large language models (LLMs). AutoSpec addresses the practical challenges in three ways: (1) driving name by static analysis and program verification, LLMs serve as generators to generate candidate specifications, (2) programs are decomposed to direct the attention of LLMs, and (3) candidate specifications are validated in each round to avoid error accumulation during the interaction with LLMs. In this way, AutoSpec can incrementally and iteratively generate satisfiable and adequate specifications. The evaluation shows its effectiveness and usefulness, as it outperforms existing works by successfully verifying 79% of programs through automatic specification synthesis, a significant improvement of 1.592x. It can also be successfully applied to verify the programs in a real-world X509-parser project.