arXiv：cs.AI· Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, Yuangang Li, Shuvendu Lahiri·· 5 小时前
Spec-Harness：评估与引导 LLM 合成的形式化规范超越可验证性
Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability
AI 导读
Spec-Harness 框架通过 Hoare 三元组符号验证和输入/输出变异，从前置与后置条件四个维度衡量 JML 规范的行为充分性。研究发现 22.7% 通过验证的规范完全没有后置条件，许多被验证器接受的规范在行为上仍然薄弱。该框架可作为反馈信号，帮助 Codex、Claude Code 及 CodeAct 风格智能体合成行为充分性更高的规范。
正文
Abstract: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.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2604.00280 [cs.SE] |
| (or arXiv:2604.00280v3 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2604.00280 arXiv-issued DOI via DataCite |
Submission history
From: Md Rakib Hossain Misu [view email]
[v1]
Tue, 31 Mar 2026 22:12:15 UTC (260 KB)
[v2]
Tue, 8 Sep 2026 22:53:51 UTC (768 KB)
[v3]
Fri, 9 Oct 2026 23:37:19 UTC (376 KB)
来源：arXiv：cs.AI · arxiv.org