Skip to content

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

🕒 Published (v1): 2026-03-31 22:12 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

VeriAct addresses a critical blind spot in LLM-based formal specification synthesis: high verifier pass rates do not imply specifications are correct or complete. The authors introduce Spec-Harness, an evaluation framework grounded in Hoare-triple reasoning and mutation testing, and VeriAct, a closed-loop agentic framework that integrates Spec-Harness feedback into iterative LLM-driven synthesis and repair of JML specifications.

Problem

Existing LLM-based JML specification synthesizers (SpecGen, AutoSpec, FormalBench prompts) treat OpenJML verifier acceptance as the primary quality signal. This is insufficient: a trivial postcondition ensures true passes any verifier yet provides no behavioral contract. Specifications can simultaneously over-constrain inputs (rejecting valid values) and under-constrain outputs (allowing any return value), all while passing verification. Additionally, LLMs may silently modify the target Java code to match the specification they produce—a failure mode no existing approach detects.

Method

The work proceeds in four stages:

  1. Empirical baseline study (RQ1): Eleven prompt configurations across six LLMs (GPT-4o, Gemini-2.0-Flash, Claude Sonnet 4.6, Qwen2.5-Coder-32B, DeepSeek-Coder-33B, CodeLlama-34B) and two classical tools (Houdini, Daikon) evaluated on SpecGenBench (120 tasks) and FormalBench (662 filtered tasks) using Verification Rate (VR).

  2. GEPA-driven prompt optimization (RQ2): Three seed prompt types (zero-shot, few-shot LtM, few-shot CoT) are evolved using GEPA (Genetic-Pareto reflective evolution) with a graduated scoring function: $\(s(r) = \begin{cases} 1.0 & \text{if verified} \\ 0.5 - \delta \cdot |E_v(r)| & \text{if syntax-clean but verification errors} \\ 0 - \epsilon \cdot |E_s(r)| & \text{if syntax errors} \end{cases}\)$ GEPA receives both the scalar score and classified error text, allowing targeted prompt repair.

  3. Spec-Harness (RQ3): An automated correctness-and-completeness evaluation framework using symbolic verification and input/output mutation testing grounded in Hoare-triple semantics. It detects over-constraining preconditions (rejects valid inputs) and under-constraining postconditions (admits incorrect outputs), independent of verifier acceptance.

  4. VeriAct (RQ4): A verification-guided agentic loop combining LLM planning, code execution, OpenJML verification, and Spec-Harness feedback in a closed repair cycle, iteratively synthesizing specifications that are verifiable, correct, and complete.

All benchmarks are normalized (classes renamed to Solution, methods to solve()) to prevent semantic leakage from identifiers. Test suites are extended to 100–200 pairs per task via automated test generation.

Key Contributions

  • Comprehensive unified comparison of classical (Houdini, Daikon) and prompt-based (SpecGen, AutoSpec, FormalBench) JML synthesizers under a common benchmark and evaluation setup.
  • Demonstration that GEPA-driven prompt optimization improves VR but hits a performance ceiling, and optimized specifications still exhibit correctness/completeness deficiencies.
  • Spec-Harness: an automated evaluation framework measuring specification quality beyond verifier pass/fail via Hoare-triple reasoning and mutation testing.
  • VeriAct: a verification-guided agentic framework that closes the gap by incorporating Spec-Harness feedback directly into the synthesis-repair loop.
  • Identification of silent code modification as an unaddressed failure mode in prior LLM-based approaches.

Results

(Paper text truncated before full RQ3/RQ4 results; only RQ1 numbers are available.)

RQ1 — Verification Rate (best configurations): - Houdini: 86.7% (SpecGenBench), 54.2% (FormalBench) — strongest classical baseline - Daikon: 18.3% / 13.1% — weakest overall - SpecGen (best): 66.7% / 30.3% - AutoSpec (best): 58.3% / 27.9% - FormalBench prompts (best): 64.2% / 36.0% - Claude Sonnet 4.6 reaches 66.7% on SpecGenBench with SpecGen 4-shot - Proprietary models (GPT-4o, Gemini, Claude) consistently outperform open-weight models at ~32–34B scale - Average VR across all configurations drops substantially from best (e.g., SpecGen: 66.7% → 43.1% on SpecGenBench), indicating high prompt sensitivity

Limitations

  • Full RQ3 (Spec-Harness) and RQ4 (VeriAct) quantitative results are not present in the provided text (paper truncated).
  • Evaluation is restricted to JML / Java; generalizability to other formal specification languages (Dafny, Coq, Lean) is unstated.
  • Test suite extension uses randomly guided automated generation, which may miss adversarial edge cases needed for thorough mutation testing.
  • Normalization removes identifier-based hints but may produce unnatural prompts that underestimate real-world LLM performance.
  • GEPA optimization is applied only to FormalBench with a 100/50/512 train/val/test split; overfitting risk for other task distributions is not analyzed.

Relevance to Harnesses / Meta-Harnesses

Spec-Harness is a direct instantiation of the harness-as-evaluator pattern: it wraps symbolic verification and mutation testing into a reusable framework that scores synthesis outputs along correctness and completeness dimensions independently of the primary verifier, functioning as a meta-evaluation layer above OpenJML. VeriAct exemplifies a meta-harness architecture where the evaluation harness is embedded inside an agentic synthesis loop—Spec-Harness feedback drives iterative LLM repair, making the harness an active controller rather than a passive scorer. This pattern—using a harness both as an oracle and as a reward signal within an agentic loop—is a generalizable design for any domain where the primary verifier is necessary but insufficient. The GEPA-driven prompt optimization stage further illustrates how graduated, structured feedback from a harness can replace scalar rewards to improve prompt evolution.