# Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability

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

## Key facts

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

## Builds on (most cited first, 30 of 31)

- [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)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learning](https://mlsanity.com/paper/2507.19457/) (2025)
- [CRUXEval: A Benchmark for Code Reasoning, Understanding and Execution](https://mlsanity.com/paper/2401.03065/) (2024)
- [Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs](https://mlsanity.com/paper/2406.11695/) (2024)
- [Multi-lingual Evaluation of Code Generation Models](https://mlsanity.com/paper/2210.14868/) (2022)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [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)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Execution](https://mlsanity.com/paper/2408.13001/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (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)
- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications](https://mlsanity.com/paper/2409.12866/) (2024)
- [A Comparative Study of DSPy Teleprompter Algorithms for Aligning Large Language Models Evaluation Metrics to Human Evaluation](https://mlsanity.com/paper/2412.15298/) (2024)
- [Beyond Code Generation: Assessing Code LLM Maturity with Postconditions](https://mlsanity.com/paper/2407.14118/) (2024)
- [Fuzzing Class Specifications](https://mlsanity.com/paper/2201.10874/) (2022)

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

- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Containment Verification: AI Safety Guarantees Independent of Alignment](https://mlsanity.com/paper/2605.09045/) (2026)

## 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. Mutation-based completeness scores go further, but they return a single number and cannot tell a generator which clause to fix. In this work, we first compare classical and prompt-based JML synthesis under a unified setup, and find that 22.7% of the verified specifications have no postcondition at all, and that prompt optimization through verification feedback repairs weak prompts but does not go beyond the best hand-written one. 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 on systematically built test suites. Spec-Harness reveals that many verifier-accepted specifications 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 on held-out tests. This holds for the general-purpose agents Codex and Claude Code and for a CodeAct-style JML synthesis agent that we built to use the verifier and Spec-Harness as feedback.