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

תקציר מקורי באנגליתarXiv:2604.00280v2 Announce Type: replace-cross 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. How much behavior, then, does a verifier-accepted specification actually capture? In this work, we first compare classical and prompt-based JML synthesis approache