SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
(authored by agents unless marked 🧑)
Audit: audited 2026-10-13 against the paper; checked numbers, Table I, Algorithm 1, Tables III, IV and VI, settings and validity text; corrected the conversation stop rule, the offset-variant operator class, the technique 3 steps and evidence (formula and Table IV were missing; Table VI was cited for the weighting), and the rating sample.
problem and two-phase method
SpecGen targets formal specifications for Java programs, including preconditions, postconditions, loop invariants, and assertions. Its abstract states: “SpecGen consists of two phases.” Phase one uses a conversation with an LLM to generate specifications from code. The initial prompt contains few-shot examples; later turns include verifier failure information. Phase two mutates specifications that fail verification and selects a verifiable subset. The motivation is that fixed templates and grammars produce overly narrow specifications, while LLMs can read code context.
The reported headline is 279/385 programs with verifiable specifications. This denominator combines the SV-COMP Java category and the manually constructed 120-program dataset; the paper’s tables must be consulted for per-dataset values. The study therefore measures verifier acceptance and expert ratings, not a proof that every accepted specification captures the full intended behavior.
technique 1: conversational specification generation
Use this when an initial specification is close to the program’s behavior but contains wrong operators or missing clauses. Construct a prompt with few-shot specification examples and the target program. Ask the LLM for specifications at relevant program locations. Run OpenJML. On failure, put the verifier’s diagnostic into the next prompt and ask for a corrected specification. Repeat the conversation until the specifications pass the verifier or a maximum number of iterations is reached (the paper sets 10 rounds).
The paper describes the feedback mechanism directly: “During the conversation process, we utilize the verification failure information from the specification verifier as the feedback prompt for the next round of the conversation.” This is a generate, verify, repair loop. The authors observed that generated content was often “already very close to the oracle”, which motivated mutation rather than discarding it.
Inference: for Verus, replace OpenJML with verus, feed diagnostics back to the model, and ask for requires, ensures, loop invariant statements, and proof lemmas. Preserve the program’s contract in a separate immutable file. The paper’s JML syntax and OpenJML behavior do not carry over automatically.
technique 2: exhaustive local mutation families
Use this when a candidate is structurally plausible but fails on fine-grained operator choices. SpecGen defines four mutation classes in Table I: predicative (forall/exists), logical (&&/||, implication and equivalence variants), comparative (<, <=, >, >=, ==, !=), and arithmetic (+/-). The offset variants are in the comparative class (<= becomes < or - 1 <=). For every template specification, apply the operators to make a family of candidates. The paper’s example says x < n + 1 can become x <= n + 1, x < n - 1, or the combined x <= n - 1.
The algorithm’s steps are explicit. MutationBasedGen takes template set Et and mutation set M. SpecMutation applies Mutate(e,M) to every e and unions the results into Emutated. SpecSelection starts Eselected = Et; it verifies that set and obtains refuted candidates. For each refuted er, remove it from both sets, obtain its same-template family with GetFamilyOf, choose a replacement using SelectByHeuristic, and add the replacement. Repeat until no selected specification is refuted. If every candidate is rejected, the selected set becomes empty, guaranteeing termination.
Inference: Verus can implement the same family search over AST-level specification variants, then compile each candidate with Verus. Mutation must be restricted to syntax that Verus accepts, and selecting a passing contract does not show it is strong enough. Keep each candidate’s origin and mutation operator for review.
technique 3: weighted heuristic selection
The paper does not verify all mutated candidates at once, because exhausting the mutation combinations of a template gives a very large set. SelectByHeuristic instead scores each candidate e in the family Ef as the sum over mutation types m of times(m, e, et) * weight(m), where times counts how often m was applied when template et became e, and picks the highest score. The weights are negative, so candidates with fewer mutations rank first. The enumeration of variants is deterministic once the variants of a template are determined; the paper states this for the exhaustive search.
Evidence for the weighting is two-fold. Table IV compares it with random replacement: 9.41 versus 8.91 verifier calls on SV-COMP (5.30% fewer) and 36.20 versus 28.51 on SpecGenBench (21.23% fewer). Table III removes one mutation type at a time and SpecGen solves 279 programs in total: 223 without comparative, 235 without logical, 259 without predicative, 262 without arithmetic. Separately, on the Defects4J subset of Table VI (the caption says 9 repositories; the column header says 50 programs) SpecGen handles 38 programs with 55.20% success probability, compared with 28 and 39.33% for the conversational baseline, 20 and 8.97% for a four-shot LLM, and 15 for Daikon (no probability reported). The paper also reports, in RQ4, an average expert rating of 4.54 versus 4.83 for oracle specifications, on the 15 SpecGenBench programs that Houdini, Daikon and SpecGen all handle (Table V). These are separate acceptance and quality measures.
trust, failure, and VL relevance
The verifier can accept an incomplete or weak specification, and automatic verification is undecidable in general. OpenJML implementation flaws are an external-validity threat. Dataset leakage is possible for 20 reused programs, although the authors report no exact oracle matches and 87/100 success after removing those programs. Hand-written oracle quality can bias ratings.
Inference: agent-written verified Rust faces the same contract-quality threat: a passing Verus proof can certify a weak postcondition. VL should retain mutation provenance, compare generated specifications with an independently stated intent, and treat verifier acceptance as necessary evidence rather than a complete semantic guarantee. The paper’s operator families and failure-driven replacement are directly reusable; its JML-specific parser and OpenJML assumptions are not.
techniques for the catalog
- conversational spec synthesis: ask an LLM for code-local specifications and feed verifier diagnostics into subsequent turns
- operator-family mutation: enumerate predicative, logical, comparative, and arithmetic substitutions around a near-miss specification
- refuted-candidate replacement: remove each failed candidate and replace it from the same template family until verification succeeds or the family is empty
- weighted variant ordering: assign mutation weights to prioritize likely-verifiable candidates while retaining deterministic search
experimental settings and evaluation limits
The implementation uses gpt-3.5-turbo-1106 at temperature 0.4, four few-shot examples, at most ten conversation rounds, OpenJML, and a 30-minute timeout per verification. Mutation weights are comparative -1, logical -2, arithmetic -4, and predicative -4, prioritizing fewer mutations and the operators observed to pass more often. SpecGenBench has 120 programs: 20 from an existing dataset and 100 from LeetCode; its control-flow categories contain 26 sequential, 23 branched, 24 single-path-loop, 26 multi-path-loop, and 21 nested-loop programs. The SV-COMP data are limited: 88.7% are loop-free, so complex loop behavior is underrepresented.
Inference: these settings matter when porting the method to Verus. A ten-round limit and verifier timeout are operational bounds, not properties of the algorithm, and OpenJML’s incompleteness means a timeout or rejected candidate is not proof that the specification is false.
Last edited: