Path2Spec: Path-Aware Specification Generation via Large Language Models

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 2-11, page and table references, the technique steps against Sections 3.1-3.2, quotations and the Verus forms; fixed one cut quotation, JPF soundness wording, Table 9 model scope, an unsupported merge-ablation claim, a nondeterminism claim the paper attributes elsewhere, and unmarked inferences.

claim and setup

Path2Spec generates Java/JML specifications by making execution paths an intermediate representation. For each path, an LLM extracts a symbolic precondition and postcondition, generates path-specific JML, verifies it with OpenJML/CVC4, repairs failures with verifier feedback, and incrementally merges verified cases. If the whole program remains difficult, it recursively decomposes the first branch and retries. On 385 programs (120 SG-Bench and 265 SV-COMP), GPT-5 reaches 325/385 = 84.4% verified specifications versus SpecGen’s 197/385 = 51.2% (Table 2, page 16). “Verified” means OpenJML exit code 0; it does not establish that the specification is complete or matches user intent.

The paper identifies the problem directly: “these methods treat a program as a single unit, resulting in overly general, coarse-grained constraints” (abstract, page 1). Its quality evaluation therefore adds human ranking and SMT comparison against ground-truth specifications. The target is Java/JML, so each Verus translation below is an inference rather than a measured result.

technique 1: extract symbolic paths before writing specifications

Use this when one prompt over a whole program produces weak or generic contracts. Ask an LLM acting as a symbolic-execution analyst to start at method entry and enumerate every path induced by conditionals, loops, and branches. For each path, require an input condition (precondition) and a symbolic output expression or state (postcondition), with no intermediate variables in the final output. The paper’s prompt ends with the schema Path [N]: Input: [condition] Output: [expression] (Section 3.1, page 9).

The path is a complete statement sequence from entry to exit, including control-flow decisions. The resulting (precondition, postcondition) pair becomes a compact behavioral case for later specification generation. Path2Spec chose an LLM because dynamic tools often produce concrete outputs tied to test coverage instead of symbolic expressions. It nevertheless compares against Java PathFinder (JPF) using a manually validated gold set.

In Verus, ask for path conditions over Rust branches and loop cases, then map each case to a requires/ensures pair or to a case lemma. Preserve symbolic expressions such as x < 0 and result == ...; do not replace them with sampled concrete tests. For loops, include the invariant and termination condition as separate proof obligations. This is an inference because Path2Spec uses Java/JML.

Direct validation on 267 gold paths gives GPT-5 91.0% correct paths, 0.4% missed, 3.4% incorrect postconditions, and 0% infeasible paths; GPT-3.5 has 67.4% correct and 15.4% incorrect postconditions (Table 7, page 21). The paper says JPF’s advantage is soundness rather than completeness: it misses 13.5% of paths (GPT-5: 0.4%) because of path-explosion cutoffs and encoding restrictions, although its Inc-Pre plus Inc-Pos rates (8.6% and 8.2%) are higher than GPT-5’s (4.1% and 3.4%) in the same table. The main failure is a wrong symbolic result, not omission, so downstream checks remain necessary.

technique 2: generate and repair one specification per path

For every extracted path, prompt the LLM with the program and that path’s precondition/postcondition. Translate path input to a JML requires and path output to an ensures; ask for loop specifications and other constructs on the path, and require coverage of all paths. Run OpenJML. If verification fails, append the error message, program, and path information to a refinement prompt. Iterate to a fixed limit (the paper’s example uses five iterations). Only after every path specification verifies do you merge them.

The paper’s generation prompt explicitly says: “Path input → requires clause as precondition” and “Path output → ensures clause as postcondition” (Section 3.1, page 10). Its refinement rules cover syntax, forbidden patterns, timeout prevention, implicit OpenJML checks, and consistency of a failed precondition or postcondition with the path. Inference: this keeps a verifier failure attached to the path that caused it rather than asking the model to repair an opaque whole-program contract.

Verus form (inference): produce a Rust contract case for each path, then prove the case with proof fns or branch-specific assertions. Use assert and assert forall to connect path conditions to outputs; use while invariants for loops. Compile and verify each case before combining them into a whole-function lemma. A Verus implementation should reject a repaired spec that silently removes the original path case or weakens its output relation.

The full pipeline’s error counts show why repair matters. Across both benchmarks, GPT-5 Path2Spec has only 2 compilation errors and 8 timeouts, against SpecGen’s 73 errors and 95 timeouts; GPT-3.5 drops from 140 single-shot errors to 33 after repair (Table 11, page 24). However, Path2Spec can expose more semantic failures after malformed outputs are repaired: GPT-5 has 50 total counterexample failures versus SpecGen’s 20. A passing verifier is still only a syntactic/basic-semantic gate.

technique 3: decompose on the first branch and retry recursively

Use this when path-specific generation still fails after the repair budget. Split the program at its first top-level branch: for if/else, switch, or a loop, decompose into two subprograms; for a loop, create one subprogram where the condition is satisfied and the body executes and one where it is false and the loop is skipped. Run path extraction and per-path generation independently on each subprogram. Recurse on a failed subprogram until all succeed, no control flow remains, or a decomposition limit is reached.

Path2Spec’s example isCommonMultiple first splits on if(m % a != 0), then recursively splits the still-hard branch on m % b != 0 (Figure 4, page 11). The method is top-down and can terminate as soon as all current subprograms pass, avoiding decomposition of branches that do not need it. If an irreducible subprogram still fails, the paper returns valid specifications for other subprograms as a partial solution and marks the original unresolved.

In Verus, split a difficult Rust function into branch-specific proof lemmas or ghost helper functions whose preconditions encode the branch. For loops, separate zero-iteration and one-or-more-iteration reasoning, but retain a general invariant for the actual loop. Merge only after each helper verifies. This is a proof-organization inference; it does not change the executable function.

Ablations show both components help. GPT-5 Path-only reaches 314/385 = 81.6%, Decomposition-only 254/385 = 66.0%, and full Path2Spec 325/385 = 84.4%; GPT-3.5 reaches 56.6%, 57.4%, and 61.8% respectively (Table 2, page 16). In Table 9 (page 23; the caption says GPT-3.5, the text says pooled over four models), at ten or more paths single-shot Path2Spec passes 62% versus SpecGen’s 24%, and with three to five branches 68% versus 45%; overall the two are close (SpecGen 52%, single-shot 50%). The limitation is cost and quality: verifier success terminates decomposition even when a deeper split might produce a more complete contract.

technique 4: merge specifications incrementally and bottom-up

After subprograms pass, merge path specifications one at a time and invoke OpenJML after each merge. For a simple program, merge path 1, verify, then path 2, verify, until all cases are in the original method. For recursively decomposed programs, first merge within each subprogram, then merge child specifications into parent programs layer by layer, ending at the original program. Record method, loop, and surrounding-line context so the merged clauses go back to the right locations.

Classify extracted clauses as Requires/Ensures, Loops (invariants, maintaining, decreases), or Others (assignable, pure, signals). Concatenate behavior cases with JML also; remove duplicate loop clauses and insert them before the matching loop; insert other clauses at the recorded contextual position. Inference: this explicit placement rule is needed because a specification copied from a subprogram can be syntactically valid in the wrong method.

For Verus (inference), merge branch lemmas into a top-level proof that dispatches on the same conditions as the executable code. Keep loop invariants at the loop and method contracts at the function boundary. Use a deterministic source-location map and re-run verification after every merge. The Verus analogue must account for Rust’s ownership and mutable-borrow structure, which JML does not model.

The paper does not test incremental merge-and-verify against a single final check, so the merge design is not supported by an ablation. Its closest result is that the single-shot form (repair loop disabled) already passes 66.2% (255/385) for GPT-5 against the full pipeline’s 84.4%, so structure supplies most of the gain over SpecGen and iteration the rest (Table 2, page 16).

technique 5: measure logical strength instead of verifier success alone

Use this when a generated contract compiles and verifies but may be too weak. First extract ground-truth and generated JML requires/ensures cases, splitting also, implications, and equivalences into logical formulas. Align cases by method signature and overlapping preconditions. Use Z3 to compare precondition domains and postcondition output ranges independently. Record a generated case as complete when its precondition is wider or equivalent and its postcondition is tighter or equivalent; record incomplete when it is narrower and looser; record undecidable when the axes conflict or Z3 cannot decide a construct.

Path2Spec evaluates 173 SpecEval pairs. For GPT-5, Path2Spec has 18 failures (10.4%), 9 incomplete cases (5.2%), 114 complete cases (65.9%), and 32 undecidable (18.5%), versus SpecGen’s 38 failures, 21 incomplete, 78 complete, and 36 undecidable (Table 6, page 20). GPT-3.5’s complete rate rises from 23.7% to 45.1%; DeepSeek-R1’s from 23.1% to 57.8%.

The paper also human-ranks 250 samples with two Java programmers on completeness, boundary coverage, constraint expressiveness, and all-behavior coverage. With GPT-5 as base model, Path2Spec averages 3.4/4 versus SpecGen 2.4/4 (Table 5, page 19); the quadratic-weighted Cohen’s kappa is 0.86 on SV-COMP and 0.46 on SG-Bench (text of Section 5.2.1, page 19). These are human judgments, not kernel proofs. In Verus, use Z3 or Verus lemmas to compare contract implication where feasible, and separately inspect boundary cases, loops, overflow, and ownership states. Do not treat “verified” as synonymous with complete.

evidence, limits, and VL threat

The strongest evidence is consistent improvement across four models and two benchmarks, but denominators matter: 84.4% is 325/385; GPT-5 SV-COMP is 220/265 = 83.0%; GPT-5 SG-Bench is 105/120 = 87.5%. The single-shot method costs about the same as SpecGen (GPT-5 overall 2.5 calls, 7.3k tokens, 51 seconds versus SpecGen 1.8 calls, 7.7k tokens, 83 seconds), while the paper says the full pipeline uses far more calls (Table 3 and Section 5.1.3, page 17). Three GPT-3.5 end-to-end runs vary from 57.4% to 69.1% on SV-COMP, mean 64.4% ± 6.2 (Table 4, page 18); the paper attributes the spread to Run 3, the originally submitted configuration, against two runs of a corrected pipeline, not to sampling randomness.

Inference: what is trusted is OpenJML/CVC4, Z3 in the logical comparison, the Java source, manually written SpecEval contracts, and path extraction/model prompts. What remains unproved is semantic equivalence of an LLM-extracted path set to all executions, completeness of a merged contract, and user intent. The paper itself says OpenJML can time out on correct specifications and that a passing specification “does not guarantee that a specification is complete” (Discussion, page 24). The work is Java/JML-specific in prompts and decomposition rules.

Inference: for VL, Path2Spec is a direct threat to agent-written Rust spec synthesis because path-wise decomposition and verifier-guided repair can substantially raise pass rates while keeping single-shot cost near a baseline. VL should reuse the intermediate path representation, recursive branch splitting, incremental merge, and separate logical-strength checks. It should not assume that Java/JML results transfer: Rust ownership, integer overflow, trait dispatch, and Verus proof idioms need dedicated path models and completeness checks.

techniques for the catalog

• symbolic path extraction — enumerate path precondition/output-expression pairs before generating contracts
• path-specific verifier repair — generate one contract per path and refine it with verifier errors until it passes or exhausts a limit
• first-branch recursive decomposition — split failed programs at their first branch or loop and retry smaller subprograms
• incremental bottom-up merge — verify each path merge and then merge child specifications into parents layer by layer
• logical-strength comparison — use SMT implication checks and human criteria to distinguish complete, incomplete, and undecidable specifications
• path-extraction benchmarking — compare LLM and symbolic extractors against a manually validated path gold set and downstream pass rates

study status

This study was written from the full extracted text of the Path2Spec PDF and is ready for the complete gate.

Last edited: 2026-10-13