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

1. Problem Statement

The paper addresses a critical gap in automated formal specification synthesis: the difference between "verifiability" and "actual quality."

• Context: Formal specifications (e.g., in Java Modeling Language, JML) are essential for software reliability. Large Language Models (LLMs) have shown promise in generating these specifications, often achieving high "verification pass rates" (i.e., the code compiles and passes a static verifier like OpenJML).
• The Core Issue: Passing a verifier does not guarantee the specification is correct (accurately reflects the intended behavior) or complete (covers all necessary constraints).
  • Trivial Specifications: A specification like ensures true (always true) will pass any verifier but provides no useful behavioral contract.
  • Over/Under-constrained: LLMs often generate specifications that are too weak (allowing invalid outputs) or too strong (rejecting valid inputs), which a standard verifier may accept if the implementation happens to satisfy the weak contract.
• Limitations of Current Approaches: Existing methods rely on binary pass/fail signals from verifiers or manual human evaluation, which does not scale and fails to detect semantic emptiness.

2. Methodology

The authors conducted a structured, multi-stage empirical study involving four key research questions (RQs):

A. Empirical Baseline (RQ1)

• Comparison: Evaluated Classical approaches (Houdini, Daikon) vs. Prompt-based LLM approaches (SpecGen, AutoSpec, FormalBench) across two benchmarks: SpecGenBench (120 tasks) and FormalBench (700 tasks).
• Setup: Used 6 LLMs (3 proprietary, 3 open-weight) and various prompt configurations (zero-shot, few-shot, CoT).
• Metric: Verification Rate (VR) – the percentage of specifications that pass OpenJML.

B. Prompt Optimization (RQ2)

• Technique: Applied GEPA (Genetic-Pareto), a reflective prompt optimizer that uses structured verification feedback (error types, not just binary scores) to evolve prompts.
• Goal: Determine if optimizing prompts can push synthesis quality beyond fixed strategies.

C. The Evaluation Framework: Spec-Harness (RQ3)

• Innovation: Introduced Spec-Harness, a new evaluation framework that moves beyond binary verification. It uses symbolic verification and mutation testing to measure four specific metrics:
  1. Post-Correctness: Does the postcondition hold for all valid test cases? (No false alarms).
  2. Post-Completeness: Does the postcondition reject mutated/incorrect outputs? (Discriminative strength).
  3. Pre-Correctness: Does the precondition admit all valid inputs? (No spurious rejections).
  4. Pre-Completeness: Does the precondition reject invalid inputs?
• Mechanism: Constructs Hoare triples for test pairs and mutants, using an SMT solver to check if the specification holds or fails, independent of the implementation code.

D. The Proposed Solution: VeriAct (RQ4)

• Framework: Proposed VeriAct, a verification-guided agentic framework based on the CodeAct paradigm.
• Workflow:
  1. Agent Planning: The LLM agent drafts a JML specification.
  2. Verification Loop: Runs verify_with_openjml. If errors occur, analyze_openjml_errors guides the fix.
  3. Quality Loop: Once verification passes, run_spec_harness evaluates the four quality metrics.
  4. Iterative Refinement: If metrics (e.g., Post-Completeness) are below a threshold, the agent receives structured feedback and revises the specification.
  5. Termination: The loop continues until the specification is both verifiable and meets the Spec-Harness quality thresholds.

3. Key Contributions

1. Comprehensive Evaluation: Demonstrated that high Verification Rates (VR) in classical and LLM-based approaches do not correlate with specification quality.
2. Performance Ceiling: Showed that while GEPA-driven prompt optimization improves VR, it hits a ceiling and fails to resolve fundamental correctness/completeness issues.
3. Spec-Harness: Developed an automated framework to measure specification quality via Meaningfully Verified Rate (MVR), exposing that many "verified" specifications are semantically empty.
4. VeriAct: Created an agentic synthesis system that closes the gap between verifiability and quality by integrating Spec-Harness feedback directly into the generation loop.

4. Key Results

• RQ1 (Baseline):

  • Houdini (Classical) achieved the highest VR (86.7% on SpecGenBench) but produced trivial specifications.
  • Prompt-based LLMs (e.g., SpecGen with GPT-4o) achieved ~66.7% VR, significantly outperforming Daikon but still lagging behind Houdini in raw pass rates.
  • Observation: Prompt-based methods are highly sensitive to prompt design (large gap between best and average configurations).

• RQ2 (Optimization):

  • GEPA optimization improved VR for weaker prompts (e.g., Zero-shot) but provided negligible gains for already strong prompts (e.g., Few-shot CoT).
  • Crucial Finding: Optimization increased the number of "verified" specs but did not fix the underlying correctness/completeness issues.

• RQ3 (Spec-Harness Analysis):

  • The "VR vs. MVR" Gap: There is a massive discrepancy between Verification Rate and Meaningfully Verified Rate (MVR).
    • Example: Houdini had an 86% VR but only 2% MVR on SpecGenBench.
    • Example: Best LLM prompts had ~50% VR but only ~24% MVR.
  • Conclusion: Most specifications accepted by verifiers are either too weak (vacuous) or incomplete.

• RQ4 (VeriAct Performance):

  • VeriAct significantly outperformed all baselines (prompt-based and optimized).
  • Improvements:
    • +5% MVR on SpecGenBench.
    • +12% MVR on FormalBench (the more complex benchmark).
  • Mechanism: VeriAct successfully identified "verify-pass but harness-fail" cases (specifications that were valid but too loose) and tightened them through iterative refinement.

5. Significance

• Paradigm Shift: The paper argues that the field must move beyond "verifiability" as the sole metric for specification quality. A specification that passes a verifier but fails to constrain behavior is functionally useless.
• Agentic Synthesis: It demonstrates that closed-loop agentic systems, which combine code execution, formal verification, and targeted quality metrics (Spec-Harness), are superior to static prompt engineering for complex formal tasks.
• Practical Impact: VeriAct provides a pathway to generating specifications that are not just syntactically correct but semantically robust, enabling better testing, model checking, and bug detection in real-world software systems.
• Open Source: The authors released the full implementation, including the Spec-Harness framework, VeriAct agent, and normalized datasets, to facilitate future research in formal specification synthesis.