Coins is introduced, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations, and finds that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis.
Abstract
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large language models (LLMs) have shown strong capabilities in theorem proving and verified code generation, their true ability to generate program specifications remains unclear. Existing evaluations require either verifying implementation conformance or proving semantic equivalence between specifications, both of which are formidably difficult and may conflate proof difficulty with specification quality. To address this problem, we introduce Coins, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations. This design aligns with the asymmetric nature of formal reasoning, where successful proofs provide reliable evidence while proof failures are inherently ambiguous. Using Coins, we conduct a large scale study on HumanEval with a curated set of human written Rocq specifications. Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality. Overall, we find that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis, and that test case based formal reasoning offers a more faithful and discriminative measure of progress.
This approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden.
Tianhai Liu, Maximilian Müller, Tobias Hey et al.· 0 citations
This work presents a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics and develops FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models.
Maarten Flippo, K. Sidorov, Tip ten Brink et al.· International Conference on...· 1 citation
Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak specifications and redundant invariants may create overconfidence in ``verified''code. We present \proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model. By analyzing proof dependencies, ProofPulse distinguishes between elements that contribute to specification intent, those used only for auxiliary checks, and those irrelevant to any proof obligation. Evaluated against an oracle of 252 programs from the dafny-synthesis benchmark, ProofPulse provides a high-precision signal for specification weaknesses, particularly unnecessary preconditions and vacuous proofs. With unsat-core minimization, ProofPulse achieves perfect precision for precondition classification and reduces false positives across all evaluated categories. These results show that proof coverage is a practical complement to verification. Although it cannot fully capture semantic intent, it can reveal weak proof coupling in programs that otherwise appear fully verified. Just as a pulse check distinguishes vitality from the mere absence of symptoms, ProofPulse exposes weaknesses in proofs that technically verify successfully but still suffer from inadequate or redundant code and specifications.
Álvaro F. Silva, Ruben Martins, Alexandra Mendes· 0 citations
This paper provides a formal account of the syntax and semantics of Hedgehog, a popular PBT framework, and proves that Hedgehog→ possesses a compositional distribution semantics, and introduces Hedgehog→, a restricted version of the language based on the arrow calculus, and proves that Hedgehog→ possesses a compositional distribution semantics.
Anthony Vandikas, Kiarash Sotoudeh, Marsha Chechik· Proc. ACM Program. Lang.· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for proving analysis completeness.
Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: A test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of "design by contract," as available in Eiffel, and exploiting a feature of modern program-proving tools based on "satisfiability modulo theories" (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and design by contract, hold significant promise to address some of the challenges of program testing, software maintenance, and automatic program repair. Moving past the traditional opposition between tests and proofs, current work on software verification treats them as complementary.
Li Huang, Bertrand Meyer, M. Oriol· Communications of the ACM· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
