SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, table total, page reference, the steps of each technique against Sec. 3, and the quotations; changed one page reference (Sec. 3.3.1 is on p. 8, not p. 7) and marked three unmarked inference passages (trusted components, the VL threat, what VL should not redo).

scope and main claim

SpecAgent is a Python prototype for synthesizing ACSL annotations for C programs. Its central claim is a workflow claim: specification generation should plan dependencies, retrieve structurally similar examples, verify candidates, repair root causes that may be upstream, and critique semantic strength after proof success. The paper evaluates this on 50 programs from 14 repositories and on 811 verification targets. It reports 96.82% precision and 88.95% recall for DeepSeek-V4, and 604/811 targets discharged. These are the paper’s measurements; the transfer to Verus below is my inference.

The paper states: “SpecAgent integrates four complementary components into a unified workflow: it analyzes program structures and dependencies to plan specification targets, leverages retrieval-augmented generation with a specification knowledge base to provide LLMs with relevant specification patterns and program context, employs agentic repairing to diagnose specification defects and revisit previously generated specifications when verification failures are traced to their dependencies, and applies an agentic critique mechanism to assess and refine semantic strength beyond proof success.” (abstract, p. 1)

technique 1: dependency-aware planning

what it is and when to use it

Before asking a model to write annotations, make a plan that identifies which functions and loops need contracts or invariants, what each property means, and how specifications depend on one another. Use this for repository code where caller/callee or loop dependencies make a locally plausible annotation insufficient downstream.

how to apply it

1. Run syntax analysis and create deterministic context containing function signatures, caller-callee relations, and loop positions.
2. Give that context and source snippets to a Planning Agent.
3. Have it list specification targets, intended semantics, dependencies, and synthesis order in natural language.
4. Use the plan as the input state for generation, and allow later critique to return REPLAN when interprocedural deficiencies are found.

The paper says: “The output of the Planning Agent is a specification synthesis plan in natural language. The plan describes the intended specification targets, their designed semantics, interdependencies, and processing order.” (Sec. 3.1, p. 6)

Verus form (inference)

A Verus implementation would construct a repository map of Rust functions, call sites, loops, traits, and relevant datatypes, then ask for a plan naming requires, ensures, invariant, decreases, and quantified facts. The plan should order foundational proofs before callers. Verus has no ACSL assigns annotation, so frame reasoning must use ownership, mutable-borrow boundaries, and explicit postconditions. The planning idea transfers; the exact C syntax and Frama-C context do not.

Evidence and limits

The ablation compares generation only with planning plus generation: DeepSeek recall changes from 80.93% to 83.99% and GPT-5 from 72.14% to 71.51%, so planning alone is not sufficient. The authors explicitly caution that ablations are not independent causal effects because components change subsequent trajectories (Sec. 6.2, p. 17). The benchmark has 50 programs, average 456.44 lines, and seven over 1,000 lines; only 14 repositories were used.

technique 2: structural retrieval-augmented generation

what it is and when to use it

Ground generation in verified examples that resemble the target’s program structure. The paper’s knowledge base contains 184 function-level units extracted from the official ACSL tutorial. Use retrieval when syntax patterns, pointers, loops, arrays, calls, or ACSL idioms are easy to get wrong.

how to apply it

1. Parse each knowledge unit and target function for parameter types, pointers/arrays, branches, loops, memory accesses, calls, return types, and ACSL constructs.
2. Encode feature presence in a 32-bit structural fingerprint.
3. Exclude units with incompatible loop structure or return type.
4. Rank the rest with popcount(Ff & Fg) / popcount(Ff | Fg) (Jaccard similarity).
5. Inject up to the three highest-ranked annotated examples into the Generation Agent prompt.
6. Permit search-and-replace edits only to annotations, then check ACSL syntax with Frama-C.

The paper says: “The Generation Agent can perform search-and-replace edits [21] to instrument candidate specifications into the target code, but is constrained by the framework to specification-level modification: the agent is only allowed to add or modify ACSL annotations, without permission to modify any code implementation itself.” (Sec. 3.2.1, p. 6)

Verus form (inference)

Store verified Rust/Verus snippets indexed by AST and semantic features: ownership mode, mutable references, slices, integer widths, loops, traits, and common quantifier patterns. Retrieve examples with a bitvector or richer embedding, but retain deterministic structural filters. Permit edits only in requires, ensures, invariant, decreases, assert, assert forall, and proof functions. A Rust verifier must reject edits to executable bodies if preserving implementation semantics is the goal.

Evidence and limits

The paper attributes full-workflow gains to component interaction, not retrieval in isolation. It does not report a retrieval-only ablation. ACSL tutorial examples may not represent Rust ownership or unsafe code. Structural overlap can select syntactically similar but semantically wrong examples, so verifier feedback remains necessary.

technique 3: verification gate and dependency-aware repair

what it is and when to use it

Treat every candidate as provisional. A gate runs Frama-C/WP, classifies syntax errors, proof failures, successes, and timeouts, and maps each failure to caller, callee, and source line. A Repairing Agent diagnoses whether the defect is local, semantic, or an upstream weak contract, edits annotations, and resubmits. Use it whenever downstream failures can originate in an earlier specification.

how to apply it

1. Parse and syntax-check the candidate.
2. Run WP and serialize outcomes as JSON.
3. Recover the failing source location and dependency context.
4. Ask the Repairing Agent to inspect source and report, then optionally run WP or Eva for extra evidence.
5. Repair syntax, inconsistent semantics, or weak upstream specifications using annotation-only edits.
6. Repeat the gate until pass or the repair budget is exhausted.

The paper says: “This turns opaque verifier-produced information into provenance-aware repair evidence, alleviating the agent’s burden concerning error comprehension and root-cause reasoning.” (Sec. 3.3.1, p. 8)

Verus form (inference)

Use cargo verus diagnostics, failed assertions, counterexample traces where available, and call-graph provenance. Repair only specification/proof code, then rerun verification. When a caller fails because a callee’s ensures is weak, reopen that callee’s contract and propagate changes. Verus diagnostics and solver behavior differ from WP/Eva, so the JSON schema and root-cause heuristics must be redesigned.

Evidence and limits

Adding repair to planning and generation raises average precision to 94.79% (DeepSeek) and 94.34% (GPT-5), compared with 89.78% and 88.66% for generation only. Full SpecAgent reaches 96.82%/88.95% and 96.10%/82.77% precision/recall. Repair can exhaust its invocation budget; solver incompleteness can make a valid candidate look failed.

technique 4: strength critique and completeness probe

what it is and when to use it

A proof only shows consistency, not that a contract says enough. After verification, a Critique Agent classifies the result as ACCEPT, IMPROVE (local weakness), or REPLAN (dependency weakness). The Postcondition Completeness Probe gives a formal test for underconstrained deterministic outputs.

how to apply it

1. Invoke critique only after the verification gate passes.
2. Inspect incomplete postconditions, overly restrictive preconditions, and trivial contracts.
3. Build a harness that calls a function twice with identical arguments and asserts equal returns: m := f(x); n := f(x); assert m = n.
4. If the equality is proved, the contract determines a unique return for each admissible input; if not, preserve the failed obligations/counterexamples as refinement evidence.
5. Send local weakness to generation; send dependency weakness back to planning.

The paper says: “If the verifier proves m = n, the contract is strong enough to uniquely determine the return value for each input, since the verifier cannot find another distinct output for the same input.” (Sec. 3.4.2, p. 9)

Verus form (inference)

For a deterministic Verus function, write a proof harness with two calls under identical preconditions and assert(m == n). Use ensures and quantified invariants to make the equality provable. For nondeterministic or stateful functions, equality is not an appropriate completeness criterion; probe the intended observational behavior instead. Verus’s executable/proof separation and ownership may require separate cloned states.

Evidence and limits

Full critique raises recall from generation-only by 8.02 points (DeepSeek) and 10.63 points (GPT-5). At two to six invocations, mean precision rises 93.11% to 96.32%, recall 87.22% to 90.01%, and gate-pass trajectories 36% to 62%; after six to eight, gains plateau around 97% precision, 90% recall, and 60–64% pass rate. The probe reasons about return determinacy, not complete heap effects or all relational properties.

orchestration, trust, and measured cost

Agents use ReAct tool calls, but a deterministic state-machine orchestrator controls role transitions, budgets, and termination. Planning and critique get ten steps; generation and repairing get thirty; total invocations are capped at ten. Agents share a workspace but no mutable conversation state. On DeepSeek, SpecAgent averages 1,684.49 seconds, 25.58 Frama-C calls, 99.40 LLM calls, and $0.6228 per program. It discharges 604/811 targets (74.5%): X509-parser 140/140, Contiki 137/163, Atomthreads 109/239, and SV-COMP 218/269. These denominators are essential: success is substantial but incomplete.

Inference: the trusted components include the C implementation, ACSL parser, Frama-C/WP and Eva, SMT solvers, model outputs, orchestrator, benchmark translations, and the equivalence script used for precision/recall. The paper notes that WP is incomplete and may create false negatives. It also reports that SpecGen modified source code and invalidated some targets (Contiki and Atomthreads); inference: this supports annotation-only edits.

Inference, for VL: the threat is high for agent-written verified Rust if the system treats “verifies” as sufficient. SpecAgent demonstrates a practical architecture for planning, retrieval, repair, and strength critique, but its C/ACSL experiments do not establish Verus correctness, unsafe-Rust coverage, or semantic adequacy of Rust contracts. VL should reuse the staged control loop and completeness probes while separately auditing ownership, panic behavior, integer overflow, unsafe boundaries, and solver assumptions.

what VL should not redo

Inference: VL need not rediscover dependency-aware planning, structural example retrieval, verifier-gated repair, or post-proof strength critique. It does need Rust-specific implementations and evidence because the paper explicitly says its evaluation focuses on C/ACSL/Frama-C and may not generalize (Sec. 6.2, p. 17).

techniques for the catalog

• dependency-aware specification planning — map functions, loops, semantics, dependencies, and synthesis order before writing contracts
• structural fingerprint retrieval — select up to three structurally similar verified examples with filtered Jaccard ranking
• provenance-aware verification repair — classify verifier outcomes, trace dependencies, repair upstream or local annotations, and rerun
• post-proof strength critique — classify contracts as accept, improve, or replan after proof success
• return-determinacy completeness probe — call a function twice on the same input and prove equal outputs to detect weak postconditions
• deterministic agent orchestration — enforce role boundaries, shared workspace exchange, and invocation budgets with a state machine

Last edited: 2026-10-13