SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 1 to 4, 6 and 10 and the relative changes in Table 2, the seven construction steps, the reward stages, the ablation and the page references; changed: the claim that the abstract gains do not match Table 2 (they are the unrounded Pass@8 values and match), the source of the cost figures (section 4.2.4, p.8, not Table 6), the page of the coverage quotation (p.9), the ablation scope (one 1.5B backbone, two reward components, not the two safeguards), and Inference marks on the trusted-base sentence.

what is proved and measured

SpecRL trains a model to generate Dafny specifications and auxiliary annotations for an existing implementation. The paper’s core distinction is between soundness (the implementation satisfies the contract) and completeness (the contract excludes implementation-impossible behaviors). It states: “However, verifier feedback alone is a poor training signal for specification synthesis: verification can prove that a specification is sound for the implementation, yet it cannot tell whether the specification is too weak.” (Abstract, p.1). The method adds execution-backed negative tests, called spectests, and rewards verified candidates by the fraction of spectests they reject.

The principal held-out result is on DafnyComp-Spec, an out-of-distribution benchmark. For the 7B Qwen2.5 model, SpecRL improves completeness over supervised fine-tuning by 33.9% at Pass@1 and 26.5% at Pass@8, and verifiable rate by 91.2% and 50.0%, respectively (Table 2, p.8). These are relative changes from the 7B SFT row, whose absolute completeness is 18.15% at Pass@1 and 21.35% at Pass@8, and whose verifiable rate is 5.44% and 11.21%; SpecRL’s absolute values are 24.30%, 27.00%, 10.40%, and 16.81%. On DafnyBench-Spec, the 7B SpecRL row is 26.40%/40.19% verifiable and 16.54%/24.17% complete at Pass@1/8 (Table 3, p.8). The paper’s abstract gives relative gains of 49.96% in verification success and 26.46% in completeness for the 7B model on DafnyComp-Spec; these are the Pass@8 values of Table 2 before rounding (16.81/11.21 and 27.00/21.35), so they agree with the table’s 50.0% and 26.5%.

technique 1: turn executions into spectests

When to use it: use this when a verifier proves a contract but cannot tell whether the contract admits impossible outputs. It is especially useful for deterministic methods whose concrete output can be observed and then mutated.

Steps from §3.3 (pp.3–5):

1. Extract one primary executable method from a Dafny file (§3.3.1). Keep other declarations as context.
2. Construct SpecCheck from the method contract (§3.3.2). Conjoin ensures clauses. Fold requires into the predicate with implication, producing (R1 && R2) ==> (E1 && E2) so inputs outside the precondition are accepted vacuously.
3. Compile SpecCheck; exclude predicates that cannot execute, including ghost-dependent or unbounded constructs (§3.3.3).
4. Ask an LLM for diverse concrete inputs covering paths, boundaries, and values near or outside requires (§3.3.4). Execute each input on the original method to obtain the observed output, retrying failed inputs for up to three reflect-and-fix rounds.
5. Ask an LLM for wrong outputs targeting boundary, off-by-one, corner-case, and plausible weak-specification behaviors (§3.3.5). Build tests that run the method, overwrite the result with the mutation, and assert !SpecCheck(input, mutated).
6. Assemble the source, predicate, and tests and execute them (§3.3.6). The rejection fraction is the empirical completeness score.
7. Ask an LLM to inspect escaped impossible behaviors (§3.3.7). If it finds weaknesses, feed them back into input and mutation generation and rebuild the suite; stop when it judges the suite adequate.

The Max example makes the mechanism concrete. For input [3,1,4,1,5] with observed output 5, mutations 14 and 100 target a missing membership condition; mutation 3 targets a non-maximum result. An empty array with mutation 99 targets the too-strong requires a.Length > 0. The weak specification rejects only one of four tests (1/4 = 0.25), while the stronger specification rejects 3/4 = 0.75 (§3.2, p.3). The paper says: “SpecRL chooses these output mutations to target plausible specification weaknesses, such as missing empty-array behavior or omitting the condition that the returned value should be an actual element.” (§3.2, p.3).

Verus form: Inference: for a deterministic Verus function, generate concrete inputs, run the executable Rust body, mutate output state or returned values in a harness, and check a runtime predicate equivalent to the candidate requires/ensures. Inference: a Verus spec fn may be non-executable, so the runtime backend applies only to executable projections; for richer contracts use verifier-backed obligations. Inference: preserve the distinction between actual outputs and mutated outputs, and gate acceptance on the original Verus proof.

Evidence and limits: the offline suites cover 5,002 programs and contain 58,256 spectests, about $250 in API cost (§4.2.4, p.8). The average suite sizes are 11.64 for 4,663 Py2Dfy-Spec programs, 12.56 for 232 DafnyComp-Spec programs, and 9.90 for 107 DafnyBench-Spec programs (Table 1, p.6). A finite suite is not a completeness proof: “Thus, even if a specification rejects all generated spectests, this does not formally prove that it is fully accurate.” (§4.4.1, p.9).

technique 2: progressive GRPO reward with a verification gate

When to use it: use this to train specification synthesis so that accuracy feedback does not reward unverifiable or vacuous contracts.

For each sampled candidate, apply four stages (§3.4.1, pp.5–6):

1. Extract valid Dafny code: reward 0.05 if extraction succeeds.
2. Compile and type-check: add 0.15 if compilation succeeds.
3. Verify against the original implementation: add 0.30 if Dafny verification succeeds; otherwise skip Stage 4.
4. Execute the fixed spectest suite and add 0.50 * rejected/total.

Thus the maximum is 1.0. The paper gives the exact equation: “r = rextract + rcompile + rverify + rspectest” (§3.4.1, p.5). GRPO samples a group of eight responses and computes each response’s advantage against the group mean and standard deviation (§2.3, p.3; §4.1.4, p.7). Penalize task bypasses: a candidate containing assume or changing the implementation receives zero. Also penalize vacuous ensures true and requires false (§3.4.2, p.6).

The ablation tests the spectest stage and the verification stage of the reward, not the two shaping safeguards of §3.4.2, and it runs on one backbone only, Qwen2.5-1.5B, because each row needs a separate RL training run (§4.2.2, p.7). On Qwen2.5-1.5B (its SFT row equals the DafnyComp-Spec row of Table 2), removing the spectest stage drops completeness from 22.24% to 19.11% at Pass@1 and from 24.71% to 21.79% at Pass@8; removing the verification gate raises completeness to 29.42% and 36.27% but drops verifiability from 4.42%/7.33% to 1.56%/2.59% (Table 4, p.8). Inference: whether the same holds at 3B or 7B is not tested. The paper concludes: “The spectest reward and verification gate play complementary roles.” (Finding 2, p.8).

Verus form: Inference: use a Rust/Verus generation loop with parsing, compilation, verus proof success, and a behavior-test score. Keep a candidate’s test score at zero unless the Verus proof passes. Reject assume-based bypasses and implementation edits according to the product’s task definition. Inference: do not treat runtime test rejection as proof; it is a ranking signal after formal verification.

technique 3: choose runtime or symbolic spectest checking

Runtime checking compiles an executable SpecCheck and runs dafny test --no-verify; it is deterministic and fast but cannot handle non-executable specifications (§Appendix C, pp.13–15). Symbolic checking creates a separate verifier obligation for each mutated behavior; it handles ghost and quantifier-heavy clauses but is slower and error counts are unstable. On ten randomly selected programs, runtime checking averages 961.95 ms overall and symbolic checking 7,704.09 ms, an 8.01× slowdown (Table 10, p.15). On DafnyComp-Spec alone, symbolic checking is 14.26× slower (13,487.11 ms versus 945.65 ms). The authors therefore use runtime checking for online RL.

Verus form: Inference: prefer executable harness checks for training throughput when contracts expose executable predicates. For non-executable Verus specifications, encode each mutation as a proof obligation and use pass/fail rather than raw error-message counts; measure its cost separately.

what stays trusted and threat to VL

Inference: the method trusts the original implementation, input generator, mutation generator, execution semantics, Dafny compiler/verifier, GRPO implementation, and the assumption that finite mutations target meaningful weaknesses. The construction filters away 17.0% of Py2Dfy-Spec programs and 7.1% of DafnyBench-Spec programs because executable SpecCheck cannot be built (§4.4.2, p.10; counts 1,146 of 6,761 and 34 of 480 in Appendix B.2, Table 9). Public benchmark contamination is also acknowledged (§4.4.3, p.10).

Inference: the threat to agent-written verified Rust is high where a weak contract can make callers unverifiable or falsely permissive. VL can adopt spectests as a post-proof contract-strength signal, but it must retain human intent review and verifier gating. Inference: the product should record denominator, model size, pass protocol, suite size, and whether scores are empirical or formally proved.

techniques for the catalog

• execution-backed spectests — mutate observed outputs into implementation-impossible pairs and score contracts by rejected mutations
• progressive gated reward — reward extraction, compilation, proof, then spectest rejection, with proof required before accuracy credit
• weakness-directed suite enhancement — ask for escaped impossible behaviors and regenerate targeted inputs and mutations
• runtime/symbolic backend choice — use executable checks for speed and verifier obligations for non-executable specifications

Last edited: 2026-10-13