Source note
VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
Summary
This paper argues that verifier pass rate is a weak target for formal specification synthesis and introduces VeriAct to generate JML specs that are verifiable, correct, and complete. It also proposes Spec-Harness, an evaluation method that checks whether verifier-accepted specs actually capture program behavior.
Problem
- The task is automatic synthesis of formal Java Modeling Language (JML) specifications for Java methods.
- Existing systems often judge success by whether OpenJML accepts the specification, but a verifier can accept specs that are too weak, partial, or wrong.
- This matters because weak specifications miss real behavior, reject valid inputs, or allow invalid outputs, which hurts verification, testing, and software reliability.
Approach
- The authors first compare classical methods (Daikon, Houdini) and prompt-based LLM methods (SpecGen, AutoSpec, FormalBench prompts) on two benchmarks: SpecGenBench and FormalBench.
- They then apply GEPA prompt optimization, using structured verifier feedback instead of a simple pass/fail reward, to improve prompt-based synthesis.
- They introduce Spec-Harness, an automated evaluation framework that checks specification correctness and completeness through symbolic verification plus input/output mutation-style checks grounded in Hoare-triple reasoning.
- They propose VeriAct, an agentic closed loop where an LLM plans and writes specs, runs code and verification tools, reads Spec-Harness feedback, and iteratively repairs the spec until it better matches the method behavior.
Results
- Dataset size: 120 tasks from SpecGenBench and 662 usable tasks from FormalBench after filtering from 700.
- Classical baselines on verifier pass rate: Houdini reached 104/120 (86.7%) on SpecGenBench and 359/662 (54.2%) on FormalBench; Daikon reached 22/120 (18.3%) and 87/662 (13.1%).
- Best prompt-based verifier pass rates were lower than Houdini: SpecGen 80/120 (66.7%) and 200/659 (30.3%); AutoSpec 70/120 (58.3%) and 185/662 (27.9%); FormalBench prompts 77/120 (64.2%) and 238/662 (36.0%).
- Prompt sensitivity was large. For SpecGen, average verifier rate dropped from the best setting to 43.1% on SpecGenBench and 20.1% on FormalBench.
- The main qualitative claim is that many verifier-accepted specifications, including prompt-optimized ones, are still incorrect or incomplete when checked by Spec-Harness.
- The excerpt states that VeriAct outperforms prompt-based and prompt-optimized baselines on correctness and completeness across two benchmarks, but it does not include the final VeriAct numeric gains in the provided text.