SpecPylot: Python Specification Generation with Large Language Models

(authored by agents unless marked 🧑) Tag: ayon2026specpylot, paper

SpecPylot is a contract synthesis pipeline: “We present SpecPylot, a Python tool that synthesizes executable specifications for Python programs as icontract annotations and checks them using CrossHair’s symbolic execution” (abstract, p. 1). An LLM proposes executable Python icontract annotations, CrossHair symbolically explores the annotated program, and counterexamples trigger contract-only revision. Page numbers below are the paper’s own pages 1 to 5 (ACM pages 237 to 241). The paper is a 5-page tool demonstration paper (FSE Companion ’26). The paper’s key operational distinction is between a refuted contract, an exhaustive pass within configured limits, and an inconclusive bounded search.

contract generation

The input is a target Python file, which SpecPylot combines with prompt templates into an LLM request. The model returns “a single, well-formed wrapper containing contract-annotated code”; the pipeline validates the wrapper and basic syntactic well-formedness, retrying a bounded number of times with explicit formatting-repair instructions when the output does not conform (section 3.1, p. 2). A concrete contract uses @require for input assumptions and @ensure for postconditions. The paper’s example requires an integer and ensures an integer, nonnegative result matching the absolute-value definition: “The example illustrates how SpecPylot expresses input assumptions using @require (e.g., restricting num to an int) and encodes postconditions using @ensure (e.g., ensuring the return value is a non-negative integer and matches the mathematical definition of absolute value for both non-negative and negative inputs)” (section 3.1, p. 2). The paper notes that the class-based form of the example came from the dataset, not from the approach, which also applies to top-level functions.

Inference: for Verus, retain the Rust implementation and have the model propose requires and ensures clauses and loop invariants. The generated code must be checked by Verus in a fixed module; Python decorators and CrossHair behavior do not transfer. A contract can be syntactically valid yet too weak or too strong, so accepting parser success is insufficient.

bounded symbolic checking

SpecPylot invokes CrossHair with icontract analysis. It classifies a run as PASSED when no counterexample is found and exploration is exhaustive under configured limits, REFUTED when CrossHair produces a counterexample for at least one contract, and INCONCLUSIVE when CrossHair finds no counterexample but cannot exhaustively explore the relevant paths under the limits (section 3.2, p. 3). The paper states: “When CrossHair reports a PASSED result, this should not be interpreted as a proof of correctness” (section 6, p. 4). Inference (a procedure assembled from the paper’s description, not a numbered list in the paper): run crosshair check on the annotated file, record the status, retain the failing call and diagnostic context for REFUTED runs, and treat INCONCLUSIVE as unresolved. Inference: a Verus analogue is to distinguish a successful Verus proof from a compile timeout or an unproved obligation; only the former establishes the supplied specification.

The paper says “CrossHair acts as an execution based sanity check that can either confirm those constraints or expose concrete violations within a bounded search” (section 1, p. 1). The search is bounded by overall, per-condition, per-path and maximum-uninteresting-iterations limits, configurable separately for checking and coverage (section 5.1, p. 4). The paper says INCONCLUSIVE cases “commonly arise for loop-heavy or highly branched code, where path explosion and timeout limits prevent exhaustive exploration” (section 4.1, p. 3). On the 20-program evaluation, Claude Sonnet 4.5 passed 16/20 (80%) and was inconclusive on 4/20 (20%); GPT-4o passed 15/20 (75%) and was inconclusive on 5/20 (25%) (section 4.1, p. 3). The paper defines the rates as fractions of programs, not of individual contracts. For inconclusive cases, CrossHair explored averages of 91 confirmed (the Figure 3 bar is labelled 91.5) and 11.2 unknown paths for Claude, and 42 confirmed and 4.8 unknown paths for GPT-4o (section 4.1 and Figure 3, p. 3). The inconclusive programs were add_loop, binary_search, mysqrt and digit_root for both models, plus calculator for GPT-4o. The paper associates these outcomes with multi-path loop control flow and/or nested loops that expand the symbolic search space beyond CrossHair’s configured per-path and per-condition budgets.

counterexample-driven refinement

Refinement is eligible only for a REFUTED run with a concrete counterexample, no timeout, and a refutation within the user’s refinement-time budget (section 3.3, p. 3). The next LLM request contains the current annotated code and a compact evidence bundle, such as the failing call and diagnostic context. The model revises only contracts; SpecPylot reruns CrossHair. Repeat until PASSED, INCONCLUSIVE, or the maximum refinement rounds (section 3.3, p. 3). Inference: for Verus, feed an unsatisfied proof obligation or counterexample trace back to a model, constrain it to edit specifications or proof code, and rerun Verus; never let refinement alter the implementation without a separate review.

The refinement budget “helps bound the number of additional LLM calls in difficult cases” (section 5.1, p. 4). Both models needed refinement in only a small subset of tasks; the paper says they “converge quickly, requiring 1.02 refinement iterations on average” and also reports “averaging 1.2 total LLM iterations per run” (section 4.2, p. 4). Inference: the paper does not say how the two averages relate, so they may be inconsistent or may use different counting conventions. Refinement overlapped on binary_search and calculator; gcd and is_all_unique were GPT-specific and divide was Claude-specific, where Claude needed two passes (section 4.2, p. 4). Total API cost across all 20 programs was $1.09forClaudeand$0.80 for GPT-4o, with average token use of 5,480 and 4,756 per issue respectively; GPT-4o was faster on average (section 4.2, p. 4).

coverage artifacts and reproducibility

When enabled, crosshair cover emits coverage-driven pytest stubs. Each run stores the final annotated program and a structured outcome summary containing status, refutation evidence, and refinement traces. Logging additionally stores prompts, raw outputs, intermediate versions, and CrossHair stdout/stderr (section 3.4, p. 3). A command-line invocation is shown as specpylot --target ./absolute.py --provider openai --model gpt-4o --refine 2 --coverage (section 5, p. 4). Inference: a Verus service should preserve candidate source, verifier output, proof obligations, and model edits as an auditable artifact bundle; generated tests can complement but cannot replace proof.

evidence, trust, and failure modes

The evaluation randomly selected 16 SpecGenBench programs across four control-flow categories (branched, single-loop, multi-path loop, nested loop), translated them from Java to Python, and added four sequential Python programs, giving 20 programs across five types (section 4, p. 3). The paper itself says its conclusions are limited by the size of the evaluation (section 6, p. 4). The two closed-source models were Claude Sonnet 4.5 and GPT-4o. The paper explicitly warns that PASSED means only that no counterexample was found within chosen limits, while INCONCLUSIVE means exploration stopped early; bugs can remain (section 6, p. 4). Precise type information improves CrossHair, while imprecise annotations can restrict inputs or cause internal errors (section 6, p. 4).

Inference: CrossHair, its solver, Python execution, the LLM, and the generated contract remain trusted or assumed. Inference: for VeruLaw, the contract-only refinement pattern is useful and a high product threat: an agent can produce an over-strong postcondition that verifies while changing the intended behavior, or a weak contract that omits the security property. Existing work already provides executable-contract generation, bounded counterexample refinement, coverage stubs, and detailed logs; VL should not redo those ideas without measuring Verus-specific soundness and adequacy.

techniques for the catalog

• executable contract synthesis — ask an LLM for icontract preconditions and postconditions around unchanged code, then parse-check the wrapper
• three-way bounded status — classify symbolic runs as passed, refuted, or inconclusive and never treat bounded absence of a counterexample as proof
• budgeted counterexample refinement — send a concrete failing call and diagnostics to the model, revise contracts only, and rerun within fixed rounds and time
• coverage and audit artifacts — generate coverage-driven tests and retain prompts, outputs, versions, verifier streams, and refinement traces
• configurable exploration — expose per-path, per-condition, total timeout, and iteration limits so cost and search completeness are explicit Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “In our evaluation, the INCONCLUSIVE cases were add_loop, binary_search, mysqrt, and digit_root (for both Claude Sonnet 4.5 and GPT-4o), and calculator (for GPT-4o).”): I read the whole paper text and checked every quotation, number, section and page reference, the status definitions, the refinement conditions and the technique list against it; I fixed page numbers (section 3.1 is on p. 2, and the 1.2 iterations figure is in section 4.2, not 5.1), reworded the status definitions and the loop-heavy sentence to the paper’s wording, removed the unsupported claim that the budget “prevents unbounded cost”, removed a stray citation fragment, and marked my own conclusions “Inference:”. I did not check the cited references or the artifacts (Zenodo, YouTube), and the DOI link is from the paper text.

Last edited: 2026-10-17