mlsanityData to 7 Oct 2026

Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specifications

arXiv 2604.00280 ↗First posted 31 Mar 2026cs.SE cs.AIcited by 2

Not on the map. Why?

Abstract (arXiv)

Formal specifications play a central role in ensuring software reliability, yet automatically synthesizing high-quality specifications remains difficult and often requires domain expertise. Recent work has applied large language models to generate specifications in the Java Modeling Language (JML), reporting high verifier pass rates. But passing a verifier only confirms that an implementation is consistent with a specification, not that the specification is meaningful. A trivial postcondition such as ensures true satisfies any verifier while saying nothing about the code. How much behavior, then, does a verifier-accepted specification actually capture? In this work, we first compare classical and prompt-based JML synthesis approaches under a unified setup, and find that prompt optimization through verification feedback raises pass rates but reaches a clear ceiling. We then introduce Spec-Harness, a framework that measures the behavioral adequacy of a specification along four dimensions of precondition and postcondition correctness and completeness, using Hoare-triple based symbolic verification and input/output mutation. Spec-Harness reveals that many verifier-accepted specifications, including optimized ones, are behaviorally weak, over- or under-constraining inputs and outputs in ways the verifier cannot see. Finally, we show that Spec-Harness works as a feedback signal that helps coding agents synthesize specifications with higher behavioral adequacy, including general-purpose agents such as Codex CLI and Claude Code, as well as VeriAct, a JML-specialized agent we build for this study.

Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 31 of its 44 references that are in the map. First posted on arXiv 31 Mar 2026.

Builds on

31 of 44 references.

References · 31

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2021Program Synthesis with Large Language Modelscited by 3,509
  3. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,193
  4. 2023Code Llama: Open Foundation Models for Codecited by 2,105
  5. 2024DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligencecited by 1,154
  6. 2024Qwen2.5-Coder Technical Reportcited by 1,151
  7. 2023DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelinescited by 803
  8. 2025GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learningcited by 449
  9. 2024CRUXEval: A Benchmark for Code Reasoning, Understanding and Executioncited by 294
  10. 2024Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programscited by 270
  11. 2022Multi-lingual Evaluation of Code Generation Modelscited by 158
  12. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
19 more
  1. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  2. 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 55
  3. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  4. 2023Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?cited by 53
  5. 2024SpecGen: Automated Generation of Formal Program Specifications via Large Language Modelscited by 51
  6. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  7. 2023Ranking LLM-Generated Loop Invariants for Program Verificationcited by 33
  8. 2024CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Executioncited by 31
  9. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  10. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  11. 2024Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languagescited by 16
  12. 2023Can ChatGPT support software verification?cited by 14
  13. 2025Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inferencecited by 14
  14. 2024SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specificationscited by 8
  15. 2026Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentscited by 8
  16. 2024A Comparative Study of DSPy Teleprompter Algorithms for Aligning Large Language Models Evaluation Metrics to Human Evaluationcited by 7
  17. 2024Beyond Code Generation: Assessing Code LLM Maturity with Postconditionscited by 4
  18. 2022Fuzzing Class Specificationscited by 3
  19. 2025MutDafny: A Mutation-Based Approach to Assess Dafny Specificationscited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 2.

2 papers.

  1. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 2
  2. 2026Containment Verification: AI Safety Guarantees Independent of Alignmentcited by 1

Similar, not cited

Close in wording, no citation either way

  1. 2026Intent-aligned Formal Specification Synthesis via Traceable Refinement
  2. 2026Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
  3. 2025Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications
  4. 2024Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
  5. 2026Teaching Code LLMs to Reason with Intermediate Formal Specifications
  6. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
  7. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generation
  8. 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?