1 Introduction↩︎

Formal specifications are symbolic constraints that describe expected program behavior and can be checked against executions [@BeschastnikhBSSE2011; @daikon99]. When a specification is written as an assertion, it becomes directly executable: the assertion can be evaluated on concrete program traces and used as feedback for verification, testing, debugging, and repair. Instead of only asking whether a program produces the correct final output, executable specifications can expose whether the program satisfies the properties needed to reach that output correctly.

Recent advances in Large Language Models (LLMs) have transformed software development. However, the hallucination and semantic unreliability of LLM-generated code have shifted the focus of software engineering research from merely generating code to a more fundamental question: how can we verify that generated code is correct and aligned with user intent, and how can we help repair it when it is not? Program specifications provide an important vehicle for this goal. They make the intended behavior explicit and can serve as oracles for checking, explaining, and correcting generated implementations. Unfortunately, manually writing high-quality formal specifications for LLM-generated code is labor-intensive and requires substantial programming and verification expertise. This creates a clear need for automated techniques that can generate executable formal specifications.

Recent research has shown that LLMs can generate program specifications for a given implementation, including postconditions and natural-language correctness conditions [@nl2postcond]. For example, NL2Postcond [@nl2postcond] and SpecMind [@le-etal-2026-specmind] infer postconditions from source code. HoarePrompt [@hoareprompt] uses natural-language state conditions for correctness reasoning, and SpecRover [@ruan2025specrover] extracts code intent to support repair. They demonstrate the value of specification-like reasoning, but their intermediate signals are not directly executable assertions.

First, most existing approaches derive specifications at a coarse granularity. Approaches such as NL2Postcond and SpecRover primarily focus on preconditions or postconditions for an entire method or program. End-to-end specifications are useful because they summarize boundary behavior: what must hold before execution and what should hold after the program terminates. However, they do not expose whether the main algorithm is correct at each internal step that could ensure the final correctness. In practice, developers rarely reason about non-trivial programs only through final outputs. Instead, they decompose a program into meaningful computation steps and check local semantic commitments: after preprocessing, an array should have a certain structure; after a loop iteration, an invariant should hold; etc. Whole-program postconditions often miss these internal obligations, making them insufficient for fine-grained verification, diagnosis, and repair.

Second, some LLM-based approaches can produce intermediate reasoning conditions, but these conditions are often expressed in natural language. For example, HoarePrompt-style reasoning can describe reachable program states at intermediate points, helping an LLM reason about correctness. However, natural-language specifications are difficult to execute directly. They may be useful for explanation or human inspection, but they provide limited support for fully automated workflows that require machine-checkable feedback, such as trace-based consistency checking, test-time assertion validation, fault localization, and automated program repair.

These limitations motivate a richer view of specification for LLM-generated code. Unlike prior work that treats specifications mainly as final summaries or textual reasoning aids, our goal is to teach models to produce the executable intermediate specifications that are validated by execution and selected for their ability to reject faulty behaviors.

\[\textcolor{formalboundary}{\{\mathsf{Pre}\}}\; S_0\; \textcolor{checkpointgreen}{\{\mathsf{Step}_1\}}\; S_1\;\cdots\; \textcolor{checkpointgreen}{\{\mathsf{Step}_n\}}\; S_n\; \textcolor{formalboundary}{\{\mathsf{Post}\}} .\] In this paper, we focus on assertion-style executable formal specifications: Boolean predicates inserted into source code and evaluated over concrete runtime states. Such specifications still describe the boundary behavior of the code, but they are executable constraints. The intermediate formal checkpoint specifications describe the semantic states reached by important algorithmic steps. Given a program, these checkpoint specifications are executable assertions placed inside the source code, so they can verify not only the final answer but also the path by which the program reaches it.

Toward this goal, our preliminary study shows that LLMs do not produce high-quality specifications in the intermediate checkpoints for a given program. A final postcondition mainly requires understanding the desired output behavior of the whole program, whereas a checkpoint specification requires understanding the internal algorithm, identifying meaningful program points, and expressing properties that should hold at those points. Thus, checkpoint specification generation demands a deeper form of step-by-step program reasoning. The gap exposed by our study suggests that current code LLMs may produce plausible final conditions while still lacking robust understanding of intermediate program execution. Moreover, they often produce trivial assertions, or weak conditions that are valid but provide little help for verification.

We introduce SpecCoder, a specification-aware training framework that teaches code LLMs to generate executable checkpoint specifications for a given program. SpecCoder constructs training data from correct programs, synthesized mutants, and specification-refinement traces, then trains models to produce interleaved code-and-specification outputs. The resulting specifications are executable assertions that can be evaluated on program traces for correctness. The trained/fine-tuned model supports the annotation setting (specification generation): given a program, it inserts executable checkpoint specifications. This paper makes the following contributions:

• A verification-guided training framework that uses reference programs, validated mutants, and specification-refinement traces to produce specification-aware supervision for LLMs.

• HumanExec, an execution-based benchmark for assessing specification generation on tasks with human-written buggy code, measuring both correctness and completeness.

• We empirically study the usefulness of specification-aware training in three downstream applications: specification generation, consistency checking between program intent and implementation, and program repair.

2 Motivation↩︎

2.1 Limitations of Natural-Language Specifications for Automated Verification↩︎

Natural-language specifications are widely used in recent LLM-based verification and program-repair methods because they are easy to generate, read, and communicate to developers [@hoareprompt]. For example, an LLM can describe an intermediate state with a sentence such as “the list should be sorted before merging”. Such descriptions are useful for human inspection and can guide an LLM’s reasoning about code.

However, the key limitation is that natural-language specifications are not executable. Unlike formal assertion-style specifications, they do not define precise Boolean conditions over concrete program states. Therefore, they cannot be directly checked against execution traces.

Fig. 1 illustrates this with a simplified interval-merging program. The natural-language checkpoint states that the intervals should be sorted before merging. This description is readable, but it cannot be evaluated automatically. If the implementation accidentally sorts intervals by their end point instead of their start point, an automated system cannot directly detect the violation. In contrast, the executable assertion at line 13 directly checks the required intermediate state on the concrete runtime value of intervals.

None

Natural-language specifications can also be vague or incomplete. For example, an LLM may state that “the current interval has been handled correctly” or “the merged list is updated properly.” These statements sound plausible, but they do not specify what must hold over program variables, such as whether the intervals are ordered, or whether the last interval contains the maximum end point seen so far.

This limitation weakens downstream automation. In program verification, a natural-language specification cannot be evaluated during execution. In consistency checking, it cannot provide an objective signal that an implementation violates the user intent. In program repair, it provides only weak feedback: the system may know that a final test failed, but not which intermediate semantic commitment was broken. In contrast, an executable checkpoint can expose the internal state where the computation first deviates from the intended behavior.

This motivates executable checkpoint specifications: assertions placed at meaningful program points that can be validated on executions and used as reliable verification signals.

2.2 Limitations of Code LLMs for Generating Reliable Formal Specifications↩︎

Executable checkpoint specifications address the non-verifiability of natural-language descriptions, but generating them is substantially harder than generating free-form text. A model must identify meaningful program points, infer the intended semantics of the intermediate state, determine which variables are in scope, and express the property as a syntactically valid Boolean predicate. A generated assertion that refers to an unavailable variable, fails on the correct program, or states a tautology such as assert True cannot serve as a reliable verification signal.

We thus examine whether base Code LLMs can generate reliable inline formal specifications through prompting alone. For each model, we prompt it to insert checkpoint assertions into correct programs and evaluate the generated assertions from three execution-based perspectives. Syntax measures whether the assertions are executable. Correctness measures whether they hold on correct executions. In our mutant-based evaluation, Completeness measures, operationally, whether they reject behavior-changing mutants that reach the same checkpoints and therefore provide useful verification signals.

For example, for the program in Fig. 1, a prompted model may generate a syntactically valid but weak assertion such as assert len(intervals) >= 0, which holds on both correct and faulty executions. It may also generate an overly strong assertion such as checking that intervals are already non-overlapping before the merge loop, which can fail on correct inputs. These illustrate why executable syntax alone is not sufficient: a useful checkpoint must be both valid for the intended computation and discriminative against faulty behavior.

Table 1 shows that prompting alone is insufficient for reliable formal checkpoint specification generation. Although the models often produce syntactically executable assertions, their semantic quality remains limited. For example, Qwen2.5-Coder-32B achieves 0.89 syntax validity, but only 0.63 correctness and 0.26 completeness. This indicates that many generated assertions either fail on correct executions or hold on correct executions, yet are too weak to reject buggy variants.

These results reveal a key challenge: executable assertions are not useful merely because they are well formed. They must also capture semantic properties that are valid for the intended computation and discriminative against faulty behavior. LLMs often miss this balance, producing assertions that are invalid, overly specific, tautological, or unrelated to the algorithmic state. This motivates a verification-guided training approach, where candidate assertions are refined using execution feedback and chosen for both correctness and discriminative power.

2.3 Key Idea↩︎

These observations suggest that checkpoint specification generation should not be treated as a purely textual generation problem. A useful checkpoint must be validated on correct executions and challenged against faulty executions. This motivates our key idea to turn specification generation into verification-guided learning. Instead of treating an assertion as useful because it appears plausible to an LLM, we evaluate candidate assertions through execution. A checkpoint specification is useful only when it satisfies two properties: it should hold on correct executions, and it should reject faulty executions that reach the same checkpoint.

Given a programming problem \(x\) and an implementation \(y\), checkpoint specification generation produces an annotated program \(\tilde{y}\), where assertions are inserted at internal program points. Each assertion \(s\) is a Boolean predicate over variables in scope at its insertion point. We evaluate these assertions on two execution populations: correct executions, where the assertions should hold, and mutant executions, where strong assertions should expose behavior-changing faults. This converts specification generation from a purely generative task into a feedback-driven process in which the quality of a specification can be checked by running the program.

3 SpecCoder: A Verification-Based Model↩︎

3.1 Data Construction↩︎

We present SpecCoder, a training framework for adapting CodeLLMs to generate executable checkpoint specifications. Given a programming problem and a program, SpecCoder constructs supervision from assertions that are validated by execution rather than accepted solely from LLM output.

The pipeline consists of four stages. First, we select reliable reference programs from a LeetCode-style programming system by keeping only submissions that pass their available test suites. These executions provide the correct runtime states on which checkpoint assertions should hold. Second, we construct behavior-changing mutants from each reference program and retain only non-trivial mutants that pass at least one test and fail at least one test. These mutants provide controlled faulty executions, excluding equivalent variants and programs that are too broken to yield useful intermediate signals.

Third, a teacher model generates checkpoint specifications through a multi-turn Explore–Submit process. At each turn, candidate assertions are instrumented and executed on the reference program and retained mutants. The verifier reports syntax errors, unsafe assertions, unreachable checkpoints, assertion failures, and mutant-rejection evidence. A submitted annotated program is accepted only when its assertions satisfy the required correctness and completeness thresholds. Finally, the accepted annotated programs are converted into supervised fine-tuning examples for two tasks: inserting checkpoint specifications into an existing program and generating a complete specification-bearing solution from the problem statement. This ensures that the student model learns from checkpoint specifications that are reachable, executable, valid on reference executions, and challenged by behavior-changing mutants.

Fig. 2 illustrates the data construction pipeline, and Algorithm 3 gives its procedural form. Starting from problems, submissions, and test suites, we select validated reference programs, generate behavior-changing mutants as controlled faulty executions, and use multi-turn specification refinement to synthesize executable checkpoint assertions. Candidate specifications are executed on both reference programs and retained mutants, and only annotated programs satisfying the correctness and completeness thresholds are kept for training.

3.1.1 Problem Selection and Reference Validation↩︎

Given a programming problem \(x_i\), we collect a human-written submission \(y_i\) and its test suite \(T_i\). To ensure that the constructed specifications are grounded in executions, we keep a sample only when two conditions are satisfied. First, the test suite must contain more than 30 tests, so that execution feedback covers more than a small number of examples. Second, the submission must pass all available tests: \(\forall t \in T_i,\quad \mathrm{Exec}(y_i,t)=\mathrm{Pass}.\) This step gives us a trusted reference implementation. The executions of \(y_i\) define the correct runtime states on which checkpoint specifications should hold. The same reference program is also used as the base program for constructing behavior-changing mutants. All train/validation/test splits are performed at the problem level before mutant generation and specification refinement. Thus, mutants and annotated programs derived from a problem cannot appear in training.

3.1.2 Mutant Generation↩︎

After validating the reference program, we construct mutants to provide negative executions. For each executable statement in \(y_i\), we prompt an LLM to generate plausible one-line buggy replacements. The prompt asks for natural coding mistakes, such as using an incorrect condition, updating the wrong variable, calling an incorrect helper function, or omitting a necessary update. Each mutant must preserve syntax while changing program behavior.

We run every generated mutant on the same test suite \(T_i\). We keep only non-trivial mutants that pass at least one test and fail at least one test: \(0 < \#\{t \in T_i \mid \mathrm{Exec}(m,t)=\mathrm{Pass}\} < |T_i|.\) A mutant passing all tests is likely equivalent to the reference program under the available tests, while a mutant that fails all tests is often too broken to provide useful intermediate signals. We also deduplicate mutants with the same pass/fail pattern over the test suite. The remaining mutants form the retained mutant pool \(\mathcal{M}_i\). They serve as controlled faulty executions: a useful checkpoint specification should hold on the reference program but reject at least some faulty executions.

3.1.3 Multi-turn Specification Refinement↩︎

Inspired by the multi-turn refinement strategy of SpecMind [@le-etal-2026-specmind], we generate executable checkpoint specifications through a verification-guided Explore–Submit process. For each task \(i\), the teacher model is given the problem statement \(x_i\), a validated reference implementation \(y_i\), the available functional tests \(T_i\), and a pool of retained behavior-changing mutants \(M_i\). The goal is to insert inline checkpoint specifications into \(y_i\) while leaving the executable implementation unchanged.

At each turn, the teacher either explores candidate checkpoints or submits an annotated program for acceptance. Regardless of the turn type, the verifier executes the candidate annotations on both the reference program and retained mutants, producing feedback on reachability, correctness, and mutant rejection. The difference is that an EXPLORE turn uses the feedback only to guide the next revision, while a SUBMIT turn additionally triggers the acceptance test against the predefined quality thresholds. The implementation code is required to remain byte-equivalent after removing assertion comments; turns that modify executable code or contain unsafe assertion expressions are rejected and regenerated.

We first extract all assertion comments from the annotated program and instrument them as executable runtime checks. Each assertion is evaluated at its original program location by wrapping its Boolean expression in a trace function. This records both whether a checkpoint is reached and whether the assertion holds every time it is reached. Assertions that contain syntactic errors, refer to undefined state at runtime, or use unsafe operations such as mutation, I/O, randomness, or dynamic evaluation are treated as invalid feedback.

3.1.3.1 Correctness

Correctness measures whether a generated checkpoint specification is valid on the reference implementation. Let \(S_i=\{s_{i1},\ldots,s_{ik}\}\) be the assertions extracted from a candidate annotated program. For assertion \(s_{ij}\) and test \(t\in T_i\), let \(r_{ijt}\) be the number of times the checkpoint is reached during the reference execution, and let \(p_{ijt}\) be the number of those evaluations for which the assertion is true. The per-assertion correctness score is \[\mathrm{Corr}_{ij} = \frac{ \sum_{t\in T_i} \mathbf{1}[r_{ijt}>0 \wedge p_{ijt}=r_{ijt}] }{ \sum_{t\in T_i} \mathbf{1}[r_{ijt}>0] }.\] If the assertion is not reached by any reference execution, we set \(\mathrm{Corr}_{ij}=0\). Thus, an assertion is correct only when every reached evaluation on the reference implementation satisfies the predicate. We aggregate at the test level rather than the raw evaluation level so that a single long-running test with many repeated checkpoint evaluations does not dominate the correctness score.

3.1.3.2 Completeness

Completeness measures whether a correct checkpoint specification can expose faulty intermediate states in retained mutants. A checkpoint should only be expected to reject faults that can influence the state observed at that checkpoint. Therefore, we restrict completeness evaluation to eligible mutants whose changed line occurs before the checkpoint and whose execution can reach the checkpoint. We only evaluate a mutant against a checkpoint when the mutant is eligible for that checkpoint: the mutated source line must occur before the checkpoint, and the corresponding original line and checkpoint must co-reach on at least one reference execution. This prevents a checkpoint from being penalized for mutants that cannot causally affect or reach it.

For assertion \(s_{ij}\), let \(E_{ij}\subseteq M_i\) be the eligible mutants that reach the checkpoint in at least one mutant execution. A mutant \(m\in E_{ij}\) is rejected if \(s_{ij}\) fails on any reached execution of that mutant. The per-assertion completeness score is \[\mathrm{Comp}_{ij} = \frac{ \#\{m\in E_{ij}: s_{ij}\text{ rejects }m\} }{ \#E_{ij} }.\] When \(E_{ij}\) is empty, no completeness claim is made for that assertion and is excluded from the averaged completeness score.

The verifier reports per-assertion feedback after each turn, including reachability, correctness, mutant rejection counts, skipped mutants, and surviving mutants when available. The teacher uses this feedback to preserve reliable assertions, repair false or unreachable ones, and strengthen assertions that are correct but weak.

The acceptance test is applied at the assertion level rather than only to an average score. This prevents a submitted program from being accepted because a few strong checkpoints compensate for invalid, unreachable, or weak ones. A submitted annotated program is accepted only if its assertions satisfy the quality thresholds. That is, every generated assertion must be reached on the reference implementation and satisfy \(\mathrm{Corr}_{ij}\geq \alpha,\) and every assertion with an evaluable mutant set must satisfy \(\mathrm{Comp}_{ij}\geq \beta,\) with at least one assertion receiving a non-vacuous completeness evaluation. In our implementation, the default thresholds are \(\alpha=1.0\) and \(\beta=0.9\). If no submitted program satisfies these conditions within the maximum number of turns, the trajectory is marked unsuccessful and is not used as accepted specification supervision.

3.1.4 Training Data↩︎

Accepted annotated programs are converted into two supervised fine-tuning tasks: specification generation and code generation.

3.1.4.1 Specification generation

This task teaches the model to insert executable checkpoint specifications into an existing program. The input contains the problem statement and a program \(p_i\), where \(p_i\) can be either the validated reference program or a retained mutant: \[p_i \in \{y_i\} \cup \mathcal{M}_i .\] For the reference program, the target is the accepted annotated program \(\tilde{y}_i\). For a mutant, we construct the target \(\tilde{m}\) by inserting the accepted checkpoint specifications at the corresponding program locations of the mutant, while preserving the mutant’s executable code. The target assertions describe the intended intermediate semantics of the task, not the behavior of the buggy code. Thus, when \(\tilde{m}\) is executed, some assertions may fail and expose the fault. The training example is the same program annotated with executable checkpoint specifications: \[(x_i, p_i) \rightarrow \tilde{p}_i .\]

3.1.4.2 Code generation

This task teaches the model to generate a specification-bearing solution directly from the problem statement. The input contains only the problem statement, and the output is the validated reference solution annotated with checkpoint specifications: \(x_i \rightarrow \tilde{y}_i .\) The final training data is the union of the two task datasets: \[\mathcal{D} = \mathcal{D}_{spec} \cup \mathcal{D}_{code}.\]

3.2 Model Training↩︎

SpecCoder is trained with supervised fine-tuning on the constructed instruction data. The training set contains two types of examples: specification-generation examples, where the model annotates a given program with executable checkpoint assertions, and code-generation examples, where the model generates a complete solution together with checkpoint assertions. The two tasks share the same goal: the response should be a program with intermediate specifications.

All examples are formatted as instruction-response pairs. For specification generation, the instruction contains the problem statement and an input program; for code generation, the instruction contains only the problem statement. In both cases, the response is the final annotated program. We do not train the student model to reproduce the teacher’s exploration turns or verifier feedback. The multi-turn refinement process is used only to construct and filter high-quality supervision targets.

With the training corpus \(\mathcal{D} = \mathcal{D}_{spec} \cup \mathcal{D}_{code},\) we optimize the standard autoregressive language-modeling objective over the target response: \[\mathcal{L}(\theta) = - \sum_{(u,o)\in \mathcal{D}} \sum_{j=1}^{|o|} \log p_{\theta}(o_j \mid u, o_{<j}),\] where \(u\) is the instruction input and \(o\) is the annotated-program response. At inference time, the trained model can be used in the specification-generation setting to insert checkpoint assertions into a given program.

4 HumanExec Dataset↩︎

We introduce HumanExec, a benchmark for evaluating whether models can generate and use executable specifications in realistic programming tasks. HumanExec is collected from recent Codeforces problems and is kept separate from the LeetCode-style data used to construct SpecCoder’s training corpus. Each task contains a problem statement, input/output specification, reference solution, human-submitted buggy solutions, and an executable test suite. The buggy programs come from real human submissions rather than synthetic mutation rules. Thus, the benchmark captures common programming mistakes in algorithm design, boundary handling, state updates, data-structure usage, and case analysis. This allows us to test if executable checkpoint specifications are useful beyond the synthetic mutants used during training-data construction.

To make the benchmark suitable for semantic verification, we filter out shallow failures. We remove submissions that do not compile, use malformed input/output handling, or fail only due to immediate runtime errors. We retain bugs that execute normally but produce incorrect outputs on some tests, since these cases require reasoning about the intended algorithm rather than merely fixing syntax or crashes. We also validate each reference solution against the available test suite and keep only tasks whose reference program passes all tests. For a buggy submission, we retain only non-trivial incorrect programs that pass at least one test and fail at least one test. This ensures that the benchmark focuses on semantic deviations rather than equivalent solutions or completely broken code.

HumanExec is aimed to measure both specification quality and downstream programming performance under a shared execution setting. It has a total of 150 tasks, each has 48–279 test cases with mean=79.53 and median=70. The number of mutant per task is 150, with min=3, max=188, mean=53.19, and median=44. The difficulty level is from 800-2500 (CodeForces standard), with mean=1348, and median=1300.

Specification generation. Given a problem statement and a reference solution, the model must insert executable checkpoint specifications at meaningful internal program points. This subtask evaluates whether generated assertions are executable, valid on correct executions, and discriminative against faulty executions from human-submitted buggy programs.

Program repair. Given a problem statement and a human-submitted buggy solution, the model must produce a repaired solution that passes the test suite. This subtask tests whether executable checkpoint specifications can provide useful local evidence for identifying and correcting semantic errors.

Program correctness checking. Given a problem statement and a candidate solution, the model must determine whether the solution is correct. This subtask evaluates whether models can use specification to justify correctness or expose a bug, instead of relying only on surface-level code plausibility.

5 Empirical Evaluation↩︎

We evaluate SpecCoder from different perspectives: whether it generates higher-quality executable checkpoint specifications for a given code, and whether these specifications improve downstream programming tasks. Our evaluation is centered around the following research questions:

• RQ1: Specification Generation. Can SpecCoder generate more correct and discriminative checkpoint specifications than prompted base models for a given code?

• RQ2: Program Correctness Checking. Can SpecCoder’s checkpoint specifications help models judge whether a candidate program is correct?

• RQ3: Program Repair. Do executable checkpoint specifications improve code repair of buggy programs?

3pt

5.0.1 Datasets↩︎

We use HumanExec as the primary benchmark for all three RQs. For RQ1, we evaluate specification generation on reference solutions. Generated assertions are executed on correct reference executions to measure validity and correctness, and are evaluated against faulty executions to measure discriminativeness. These faulty executions are obtained from human-submitted buggy solutions in HumanExec; if evaluation-only mutants are additionally used, they are generated only after the train/test split and are never used for training. For RQ2, we construct candidate programs from both reference solutions and human-submitted buggy solutions and ask models to predict if each candidate is correct. For RQ3, we use human-submitted buggy solutions as repair inputs and evaluate generated repairs against the HumanExec test suites.

5.0.2 Models↩︎

We evaluate representative LLMs from the Qwen2.5-Coder families: Qwen2.5-Coder-7B, Qwen2.5-Coder-14B, Qwen2.5-Coder-32B. For each model, we compare the base instruction-tuned model with its SpecCoder-tuned counterpart. All methods use the same decoding settings and evaluation test suites.

5.1 RQ1: Specification Generation↩︎

5.1.1 Baselines↩︎

We compare SpecCoder against zero-shot specification generation, where the base instruction-tuned model directly annotates a given program with checkpoint specifications. This baseline tests whether prompting alone is sufficient to produce high-quality executable specifications from the same backbone model.

5.1.2 Metrics↩︎

We evaluate generated specifications using execution-based metrics. Validity measures the fraction of generated assertions that can be safely instrumented and executed, excluding assertions with syntax errors, out-of-scope variables, or unsafe operations. Correctness measures whether a reachable assertion holds on correct executions of the reference solution. Completeness measures, in an operational mutant-based sense, whether a correct assertion rejects behavior-changing faulty executions that reach the same checkpoint. Completeness is measured using evaluation-only behavior-changing mutants constructed from HumanExec reference solutions after the train/test split. These mutants are used only for evaluation and are not included in SpecCoder’s training data. Note that completeness captures discriminative power against the available faulty executions rather than logical completeness over all possible bugs. We report these metrics separately for inline checkpoint specifications and final postconditions.

5.1.3 Results↩︎

Table 2 summarizes the specification-generation results on HumanExec. Across the zero-shot base models, larger base models improve correctness and completeness, although validity is not strictly monotonic. Yet, their specifications remain limited. Qwen2.5-Coder-7B achieves only 0.2794 correctness and 0.1707 completeness, while Qwen2.5-Coder-14B improves correctness to 0.5227 but still obtains only 0.1989 completeness. The strongest base model, Qwen2.5-Coder-32B, further improves to 0.6313 correctness and 0.2640 completeness, yet its generated specifications are still far from reliably discriminative. These results indicate that scaling the base model helps, but prompting alone is insufficient for generating specifications that are both correct and useful for rejecting buggy executions.

SpecCoder substantially improves inline checkpoint specification quality. With Qwen2.5-Coder-14B, SpecCoder increases correctness from 0.5227 to 0.6468 and completeness from 0.1989 to 0.7713, while reaching 1.0000 executable assertion validity. With Qwen2.5-Coder-32B, SpecCoder reaches 0.8098 correctness and 0.6843 completeness, compared with 0.6313 and 0.2640 for the corresponding base zero-shot model. Across the three tuned backbones, SpecCoder improves average inline correctness from 0.4778 to 0.6306, average inline completeness from 0.2112 to 0.7459, and average validity from 0.8387 to 0.9667. These gains show that verification-guided fine-tuning teaches the model to generate checkpoint assertions that are not only syntactically executable, but also substantially more discriminative against behavior-changing mutants. The specifications from SpecCoder range from value constraints, ordering structure, loop progress, algorithm, data shape, and others.

Figure 4 further explains the source of these gains. We measure Checkpoint Quality as the fraction of assertions reached by at least one test case, and Non-triviality as the fraction of assertions that reject at least one mutant. These metrics are useful because a model could generate assertions in locations where no faulty execution reaches or can be affected by them. Such assertions may be correct, but they do not provide evidence for discriminating correct behavior from faulty behavior. Across all three backbones, SpecCoder consistently improves both metrics: average checkpoint quality increases from 68.6% to 87.1%, while the non-trivial assertion rate increases from 39.3% to 83.4%. This shows that SpecCoder does not merely generate more executable assertions; it generates assertions that are more often exercised during execution and more likely to expose faulty intermediate states.

The remaining results follow the same trend. For Qwen2.5-Coder-7B, SpecCoder achieves 0.4353 correctness, 0.7820 completeness, and 0.9028 validity, improving over the corresponding zero-shot base model by 55.8%, 358.1%, and 9.1%, respectively. For postcondition specifications, SpecCoder achieves 0.6971 correctness and 0.6062 completeness on average, compared with 0.6288 correctness and 0.2485 completeness for zero-shot prompting. The postcondition results show that SpecCoder also improves final-state specifications, but the largest gains occur for inline checkpoint completeness. This suggests that verification-guided training is especially beneficial for the harder task of generating intermediate assertions that expose faulty internal states. Overall, the results indicate that executable checkpoint specifications require verification-guided training rather than direct prompting alone.

5.1.4 Does SpecCoder Internalize Checkpoint Specifications?↩︎

We further measure whether SpecCoder internalizes executable checkpoint specifications using 30 held-out validation problems from the dataset construction process. Each problem contains verified annotated specifications produced by our verification-guided refinement pipeline. For each assertion, we teacher-force the same annotated program under the base model and the corresponding SpecCoder model, and compute perplexity only over assertion tokens. Since both models score the same target assertions, lower perplexity indicates that the model assigns higher likelihood to the same specification.

Fig. 5 shows that SpecCoder shifts the per-assertion perplexity distribution left across all three backbones, indicating higher confidence on the same executable assertions. Together with Table 2, this suggests that it learns both the syntax and placement patterns of checkpoint specifications, rather than relying only on prompting-time instruction following.

5.1.5 Qualitative Analysis↩︎

Fig. 6 shows a representative example comparing zero-shot specification generation with SpecCoder. The original model does not generate specifications in the required executable format; instead, it mainly inserts explanatory comments, such as describing that s accumulates digit sums or that t is a greatest common divisor. Even comments prefixed with “assert” are still natural-language descriptions rather than valid Boolean predicates. As a result, they cannot be directly instrumented or checked during execution. In contrast, SpecCoder generates executable checkpoint assertions over in-scope variables, such as s == 0 and N - 2 > 0, n == N and 2 <= i < N, and t > 0 and s % t == 0 and (N-2) % t == 0. These assertions are placed at meaningful internal program points and can be evaluated on runtime states, illustrating why SpecCoder improves both assertion validity and discriminative completeness.

5.2 RQ2: Program Correctness Checking↩︎

4.0pt

RQ2 evaluates whether checkpoint specifications help a model judge whether a candidate program is correct. This task is different from repair: the model must produce a correctness verdict and justification rather than a patch.

5.2.1 Baselines↩︎

We compare direct correctness checking from the problem statement and code against chain-of-thought prompting, HoarePrompt-style natural-language specification reasoning, and SpecCoder with executable assertion evidence. The SpecCoder classifier receives checkpoint specifications and, when applicable, violated-specification evidence.

5.2.2 Metrics↩︎

We report Matthews Correlation Coefficient (MCC), balanced accuracy, true negative rate, true positive rate, false negative rate, and false positive rate. MCC and balanced accuracy summarize overall classification quality under class imbalance, while FPR and FNR distinguish the risk of incorrectly accepting a buggy program from the risk of incorrectly rejecting a correct program.

5.2.3 Results↩︎

Table 3 reports correctness-checking results on HumanExec. Overall, executable checkpoint evidence improves correctness checking across model sizes. Compared with Vanilla, SpecCoder improves MCC from 0.236 to 0.307 for Qwen2.5-Coder-7B, from 0.283 to 0.384 for Qwen2.5-Coder-14B, and from 0.394 to 0.493 for Qwen2.5-Coder-32B. Balanced accuracy follows the same trend: SpecCoder achieves 0.653, 0.680, and 0.733 across the three backbones, matching or exceeding the strongest baseline in each model group. In contrast, simple chain-of-thought prompting does not reliably improve correctness checking and even reduces MCC for all three backbones. This suggests that free-form reasoning alone is insufficient, while executable specification evidence gives the checker a more reliable signal.

5.2.4 Qualitative Analysis↩︎

Figure 6 also illustrates why executable checkpoint specifications provide stronger evidence for correctness checking than natural-language state reasoning. HoarePrompt generates readable state descriptions, such as explaining that a is the GCD of the original arguments or describing the state before a function call, but these descriptions are not executable and cannot be objectively checked against a candidate program. Some conditions also refer to implicit concepts such as “original” variable values, making them difficult to bind to concrete runtime states. By contrast, SpecCoder produces executable assertions that define concrete obligations over program variables, including initialization constraints, loop-state properties, accumulated digit-sum relations, and divisibility checks after gcd. When a candidate program violates such an assertion, the checker receives localized, machine-checkable evidence of the semantic deviation, explaining the improved correctness-checking performance of SpecCoder.

5.3 RQ3: Program Repair↩︎

3.0pt

RQ3 evaluates whether executable checkpoint specifications help models repair human-written bugs. Given a buggy program, each method generates one or more candidate repairs under the AgentCoder backbone. We execute each candidate against the full test suite and measure whether the generated patch fixes the program.

5.3.1 Baselines↩︎

We introduce AssertRepair, an APR method that leverages assertion signals for program repair. Specifically, given a failing test input, AssertRepair executes the program and captures the assertion states, including violated checkpoint specifications. The resulting diagnostic evidence is then provided to the LLM to guide repair generation.

Besides the vanilla baseline, we compare AssertRepair with state-of-the-art repair baselines based on natural-language specification signals. We adopt HoarePrompt (V), which uses programs annotated with HoarePrompt-generated specifications for repair, and SpecRover (V), a competitive-programming variant of SpecRover. In contrast to these natural-language-specification baselines, AssertRepair uses executable checkpoint specifications and violated-assertion evidence. To ensure a fair comparison, all methods are allowed only a single repair attempt per turn.

5.3.2 Metrics↩︎

We report Pass@k, where \(k \in \{1,3\}\), measuring whether at least one of the top-\(k\) generated repairs passes all tests. We also report Average Pass Rate (APR).

5.3.3 Results↩︎

Table 4 reports program repair results on HumanExec. Overall, executable checkpoint evidence improves repair effectiveness, especially for the top-ranked generated repairs. SpecCoder achieves the best Pass@1 for all three backbones: 0.140 for Qwen2.5-Coder-7B, 0.241 for Qwen2.5-Coder-14B, and 0.283 for Qwen2.5-Coder-32B.

For Qwen2.5-Coder-14B and Qwen2.5-Coder-32B, SpecCoder achieves the highest APR, improving over Vanilla from 0.578 to 0.598 and from 0.615 to 0.622, respectively. These gains suggest that executable checkpoint specifications help the repair agent produce a larger fraction of passing patches, not only a better top candidate.

Averaged across the three backbones, SpecCoder obtains an APR of 0.578, compared with 0.547 for Vanilla and 0.544 for HoarePrompt. Its average APR is close to SpecRover’s 0.582, while SpecCoder achieves stronger Pass@1 and Pass@3 on average. The results therefore suggest that executable checkpoint evidence is most effective at guiding the repair process toward correct high-ranked patches, while its effect on the entire candidate distribution depends on the strength of the underlying model.

Overall, RQ3 shows that executable checkpoint specifications provide useful localized evidence for program repair. This evidence improves top-ranked repair success across all model sizes and improves average repair quality for the stronger 14B and 32B backbones.

6 Related Work↩︎

6.0.0.1 Traditional specification inference

Dynamic approaches infer likely properties by observing executions [@ammons-popl02; @BeschastnikhBSSE2011; @daikon99], but their results depend heavily on the coverage and diversity of available tests. Static analyses [@10.1145/1273463.1273487; @engler-sosp01; @kremenek06; @ramanathan-pldi07; @yiwei-icse11] and abstract interpretation [@10.1145/2384616.2384633] often produce conservative or imprecise specifications due to over-approximation and false positives. Other approaches extract specifications from API documentation or code comments [@10.5555/2337223.2337319; @10.1145/1294261.1294276; @10.1145/1985793.1985796; @10.1109/ICST.2012.106; @10.1145/3213846.3213872; @10.1109/ASE.2009.94; @7985647]. Data-mining techniques infer common API usage patterns from large codebases [@prminer-fse05; @dynamine05; @mapo09], including call pairs, sequences, and finite-state models [@zeller07; @williams-tse05; @taoxie-ase09; @fse09; @mike-ase09; @zeller-ase09]. These methods are useful for API usage constraints, but they rarely infer executable postconditions [@ramanathan-pldi07].

6.0.0.2 Machine-learning and LLM-based specification generation

Recent machine-learning and LLM-based techniques have expanded automated specification and oracle generation. Some methods synthesize test oracles or unit tests [@dinella2022toga; @mastropaolo2023usingtransfer; @10.1145/3524481.3527220; @lahiri2023interactivecodegenerationtestdriven; @tufano2021unittestcasegeneration], while others improve test generation and coverage [@lemieux2023codamosa; @coverup2025]. For example, AthenaTest [@tufano2021unittestcasegeneration] generates unit test inputs and oracles from the focal method implementation, TOGA [@dinella2022toga] focuses on oracle generation, and TiCoder [@lahiri2023interactivecodegenerationtestdriven] uses LLMs to generate inputs/outputs from textual intent.

Other work directly targets specifications. NL2Postcond [@nl2postcond] uses LLMs to infer postconditions from code and textual descriptions, and EvoSpex [@10.1109/ICSE43902.2021.00112] applies evolutionary learning to infer functional input–output relationships. Recent efforts also explore property-based specifications: Vikram et al. [@vikram2024largelanguagemodelswrite] use LLMs to generate property-based tests, while Speculyzer [@DBLP:journals/corr/abs-2210-00848] enumerates likely properties and candidate inputs to guide code generation. Beyond input–output properties, learning-based methods have been used to infer program invariants [@10.1145/2837614.2837664; @Laich2020Guiding; @10.1145/3385412.3385986; @pmlr-v202-pei23a]. In contrast, SpecCoder targets executable checkpoint specifications: assertions placed at meaningful internal program points and selected using execution feedback from correct programs and behavior-changing mutants.

6.0.0.3 Specification-guided reasoning and repair.

LLMs have been used to produce specification-like reasoning for correctness checking and program repair. HoarePrompt [@hoareprompt] uses natural-language state conditions to support structural reasoning about program correctness. SpecRover [@ruan2025specrover] extracts natural-language code intent to guide agentic program repair, vet patches, and provide supporting evidence. These approaches show that specification-like signals can improve LLM-based reasoning, but their intermediate signals are primarily expressed in natural language and are not directly executable assertions. SpecCoder differs by training CodeLLMs to generate executable intermediate specifications that can be checked on concrete executions and used as verifiable evidence for specification generation, consistency checking, and repair.

7 Conclusion↩︎

We presented SpecCoder, a verification-guided framework for training CodeLLMs to generate executable checkpoint specifications. By learning from validated reference programs, behavior-changing mutants, and refinement traces, SpecCoder produces assertions that capture intermediate program states and can be checked during execution. Experiments on HumanExec show that these checkpoints improve specification quality and provide useful evidence for correctness checking and program repair, suggesting that executable intermediate specifications are a promising path toward more verifiable and repairable LLM-generated programs.

8 Data Availability Statement↩︎

All data and code are available at [@speccoder-website].