# CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 36 references that are in the map.
- First posted on arXiv 14 Apr 2026.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generation](https://mlsanity.com/paper/2303.12570/) (2023)
- [RepoBench: Benchmarking Repository-Level Code Auto-Completion Systems](https://mlsanity.com/paper/2306.03091/) (2023)
- [CrossCodeEval: A Diverse and Multilingual Benchmark for Cross-File Code Completion](https://mlsanity.com/paper/2310.11248/) (2023)
- [Large Language Model-Based Agents for Software Engineering: A Survey](https://mlsanity.com/paper/2409.02977/) (2024)
- [SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents](https://mlsanity.com/paper/2406.12952/) (2024)
- [LeetCodeDataset: A Temporal Dataset for Robust Evaluation and Efficient Training of Code LLMs](https://mlsanity.com/paper/2504.14655/) (2025)
- [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)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [UTBoost: Rigorous Evaluation of Coding Agents on SWE-Bench](https://mlsanity.com/paper/2506.09289/) (2025)
- [EvoCodeBench: An Evolving Code Generation Benchmark with Domain-Specific Evaluations](https://mlsanity.com/paper/2410.22821/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [EffiBench-X: A Multi-Language Benchmark for Measuring Efficiency of LLM-Generated Code](https://mlsanity.com/paper/2505.13004/) (2025)
- [MHPP: Exploring the Capabilities and Limitations of Language Models Beyond Basic Code Generation](https://mlsanity.com/paper/2405.11430/) (2024)
- [Otter: Generating Tests from Issues to Validate SWE Patches](https://mlsanity.com/paper/2502.05368/) (2025)
- [A Study of LLMs' Preferences for Libraries and Programming Languages](https://mlsanity.com/paper/2503.17181/) (2025)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications](https://mlsanity.com/paper/2404.11050/) (2024)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)

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

- [Skill Drift Is Contract Violation: Proactive Maintenance for LLM Agent Skill Libraries](https://mlsanity.com/paper/2605.10990/) (2026)
- [Rules to Tools: Executable Checks for LLM Agents in Scientific Computing](https://mlsanity.com/paper/2610.00313/) (2026)
- [SpecGuard: Proving a Task Is Broken Before the Agent Cheats](https://mlsanity.com/paper/2610.09159/) (2026)
- [SpecGuardBench: Can Coding Agents Construct Reliable Validation Harnesses from Natural Language Specifications?](https://mlsanity.com/paper/2610.16870/) (2026)

## Abstract (arXiv)

Large language models (LLMs) can generate code from natural language, but the extent to which they capture intended program behavior remains unclear. Executable behavioral specifications, defined via preconditions and postconditions, provide a concrete means to assess such understanding. However, existing work on specification generation is constrained in evaluation methodology, task settings, and specification expressiveness. We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol. CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions. Constructed from diverse real-world codebases, it enables a realistic assessment of both correctness (accepting valid behaviors) and completeness (rejecting invalid behaviors). Evaluating 15 state-of-the-art LLMs on CodeSpecBench, we observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate. We further find that specification generation is substantially more challenging than code generation, indicating that strong coding performance does not necessarily reflect deep understanding of intended program semantics. Our data and code are available at https://github.com/SparksofAGI/CodeSpecBench.