Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes

Abstract

Formal specifications play a central role in ensuring software reliability and correctness. However, automatically synthesizing high-quality formal specifications remains a challenging task, often requiring domain expertise. Recent work has applied large language models to generate specifications in Java Modeling Language (JML), reporting high verification pass rates. But does passing a verifier mean that the specification is actually correct and complete? In this work, we first conduct a comprehensive evaluation comparing classical and prompt-based approaches for automated JML specification synthesis. We then investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback. While optimization improves verifier pass rates, we find a clear performance ceiling. More critically, we propose Spec-Harness, an evaluation framework that measures specification correctness and completeness through symbolic verification, revealing that a large fraction of verifier-accepted specifications, including optimized ones, are in fact incorrect or incomplete, over- or under-constraining both inputs and outputs in ways invisible to the verifier. To push beyond this ceiling, we propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications through a closed loop of LLM-driven planning, code execution, verification, and Spec-Harness feedback. Our experiments on two benchmark datasets show that VeriAct outperforms both prompt-based and prompt-optimized baselines, producing specifications that are not only verifiable but also correct and complete.

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

Abstract

Formal specifications play a central role in ensuring software reliability and correctness. However, automatically synthesizing high-quality formal specifications remains a challenging task, often requiring domain expertise. Recent work has applied large language models to generate specifications in Java Modeling Language (JML), reporting high verification pass rates. But does passing a verifier mean that the specification is actually correct and complete? In this work, we first conduct a comprehensive evaluation comparing classical and prompt-based approaches for automated JML specification synthesis. We then investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback. While optimization improves verifier pass rates, we find a clear performance ceiling. More critically, we propose Spec-Harness, an evaluation framework that measures specification correctness and completeness through symbolic verification, revealing that a large fraction of verifier-accepted specifications, including optimized ones, are in fact incorrect or incomplete, over- or under-constraining both inputs and outputs in ways invisible to the verifier. To push beyond this ceiling, we propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications through a closed loop of LLM-driven planning, code execution, verification, and Spec-Harness feedback. Our experiments on two benchmark datasets show that VeriAct outperforms both prompt-based and prompt-optimized baselines, producing specifications that are not only verifiable but also correct and complete.

Paper Structure

This paper contains 40 sections, 9 equations, 5 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Background & Motivation
  3. JML and Deductive Verification
  4. Motivating Example
  5. Research Questions
  6. Empirical Study: Classical vs. Prompt-Based Specification Synthesis
  7. Baselines
  8. Classical Approaches.
  9. Prompt-Based Approaches.
  10. Dataset
  11. Normalization.
  12. Test Suite Extension.
  13. Experiments
  14. Results
  15. Classical Approaches.
  16. ...and 25 more sections

Figures (5)

  • Figure 1: Example of a JML annotated snippet from SpecGenBench with formal specification generated by an LLM
  • Figure 2: Task category distribution (%) for SpecGenBench and FormalBench.
  • Figure 3: Verification Rate (VR%) in all prompt based approaches for all LLMs and prompt types.
  • Figure 4: Meaningfully Verified Rate (MVR), for the best prompt configurations. MVR% = % of verified task where the Spec-Harness metrics value, PostCorr >= 0.50 and PostComp >= 0.50
  • Figure 5: Verification Rate (VR%) vs. Meaningfully Verified Rate (MVR%) for the Best Configurations Prompts

Theorems & Definitions (4)

  • definition 1: Post-Correctness
  • definition 2: Post-Completeness
  • definition 3: Pre-Correctness
  • definition 4: Pre-Completeness