SKILLFORGE: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs

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

what the system does

SKILLFORGE turns natural-language-to-Dafny synthesis into six atomic skills and a deterministic verification-driven harness. The skills are specification inference, body synthesis, invariant generation, error diagnosis, targeted repair, and specification strengthening. Each skill is a triple of prompt template, tool binding, and decidable success criterion (section 3.2). The paper states the design motivation: “The key insight is that the Dafny verifier provides a formal oracle: its structured error output can be parsed into categories that deterministically select the next skill to invoke.” (section 1, PDF p. 2)

The harness starts with a natural-language instruction, constructs an initial program, runs Dafny, classifies errors, routes to a skill, and repeats under a finite budget. The paper claims it never returns an unverified program: “This holds regardless of individual skill correctness—the harness never returns an unverified program.” (section 3.3, PDF p. 5) The paper evaluates 178 NL–Dafny pairs: 42 Dafny standard library examples (tutorials and exercises), 86 DafnyBench examples, and 50 examples from open-source GitHub repositories. Difficulty counts are 62 simple, 71 medium, and 45 hard (section 4.1, PDF p. 5).

Inference: For VeruLaw, the reusable contribution is a bounded router around Verus diagnostics, not the Dafny prompts themselves. A Verus implementation would need its own error categories and skill contracts.

technique 1: atomic skill contracts

INFERSPEC extracts input and output types, preconditions, postconditions, and construct type (function, method, predicate, or lemma) from natural language. Dafny’s type checker validates the extracted fields. SYNTHBODY generates a body from the resulting scaffold, and specification anchoring explicitly forbids changing the specification. GENINVARIANT is triggered when the verifier reports that a loop body cannot establish its postcondition, and proposes invariants that (1) hold on entry, (2) are preserved by the loop body, and (3) with the negated guard, imply the postcondition; each proposed invariant is validated individually for inductiveness before insertion (section 3.2, PDF p. 4).

DIAGNOSEERROR classifies a failed verification into four categories using regex pattern matching for common messages and LLM reasoning as fallback for ambiguous cases, returning category, line, and suggestion. REPAIRCODE makes minimal edits at the identified failure site instead of regenerating the program. STRENGTHENSPEC infers implicit domain constraints such as “non-negative integer” (which becomes requires x >= 0), proposes candidate clauses, validates each individually, and then composes the validated set (section 3.2, PDF p. 4). Table 1 (PDF p. 4) gives each skill an input, tool binding, and success criterion; for example, GENINVARIANT’s criterion is “Program verifies with invariants”.

Inference: Verus form: map INFERSPEC to a structured request for requires and ensures; map GENINVARIANT to loop invariant clauses; map DIAGNOSEERROR to a classifier over Verus diagnostics; map REPAIRCODE to a constrained source edit; and map STRENGTHENSPEC to adding validated clauses. Inference: Verus has proof functions and lemmas for intermediate facts, but the router must not turn a proof-only function into runtime code or attach executable contracts to spec fn.

technique 2: deterministic routing and bounded iteration

The harness composes INFERSPEC and SYNTHBODY into an initial candidate, and if it verifies, returns immediately (section 3.3, PDF p. 4). On failure, it calls DIAGNOSEERROR and routes deterministically: invariant_missing to GENINVARIANT, spec_gap to STRENGTHENSPEC, body_error to REPAIRCODE, and type_error to SYNTHBODY (equation 5, section 3.3, PDF p. 5). Algorithm 1 (PDF p. 5) infers the specification once, synthesizes a body, then loops up to N times: verify, return on success, record the candidate with the fewest errors so far, diagnose, route, and apply the skill. If the skill returns the program unchanged (d′ = d), the algorithm instead re-runs SYNTHBODY with temperature 0.3; if the budget runs out it returns failure. Section 3.3 (4) lists the termination mechanisms: a hard iteration budget, stagnation detection (di = di−1), and a monotonicity check (“error count increasing for two rounds triggers rollback to dbest”). The paper also says the harness maintains a state Si = (di, errors i, diag i, history i) for “progress tracking and rollback”. The paper’s formal guarantee is H(x) = d* != empty implies Verify(d*) = top (equation 6, PDF p. 5). It emphasizes, “This deterministic mapping is a core distinction from agent-based systems where next-action selection relies on unconstrained model reasoning.” (section 3.3, PDF p. 5)

Inference: How to apply it: (1) infer and freeze the specification; (2) synthesize a body; (3) run the verifier; (4) classify the failure; (5) invoke the mapped skill; (6) if the skill leaves the candidate unchanged, re-synthesize at higher temperature; (7) roll back to the best candidate if errors rise for two rounds; and (8) stop at success or budget exhaustion. This list is my composition of Algorithm 1 and the section 3.3 (4) prose. Algorithm 1 as printed records the best candidate (dbest, ebest) but does not itself restore it; the rollback rule appears only in the prose.

Inference: Verus diagnostics may not have exactly these four stable categories, so VL would first need a measured taxonomy and a safe fallback when classification is ambiguous.

technique 3: equivalence checking

Beyond self-verification, SKILLFORGE compares a generated program with a reference by checking precondition equivalence (P ⇔ P̂), postcondition equivalence (Q ⇔ Q̂), and behavioral equivalence (P(x) ⇒ S(x) = Ŝ(x)), “encoded as Dafny lemmas and verified automatically” (section 3.4, PDF p. 5). Appendix F (PDF p. 17) describes a three-stage pipeline (interface matching, specification equivalence, behavioral equivalence) with an automatically synthesized wrapper lemma that asserts equal outputs under the shared precondition. The paper’s equivalence rate (ER) metric counts verified programs that are also semantically equivalent to the reference (section 4.3).

Inference: this is the paper’s only mechanism for catching verified programs whose semantics differ from the reference; the 5.1-point VR–ER gap is the measured size of that effect.

Inference: Verus form: state reference and generated behavior as spec fns, prove equality or refinement with lemmas, and call those lemmas from a proof harness. Inference: equivalence requires a trustworthy reference specification; it does not establish that either implementation matches an unstated user intent.

technique 4: structured prompt parsing and hybrid diagnosis

Appendix A gives exact prompt templates rather than free-form prompts. INFERSPEC requires fixed fields for type, name, parameters, returns, Requires, and Ensures; SYNTHBODY receives the signature and contract and is told “Do NOT modify the signature or specification” and “Do NOT weaken the postcondition”; REPAIRCODE receives a category, line, and suggestion and is told to “Make MINIMAL edits”; GENINVARIANT must produce invariants that hold on entry, are preserved by one iteration, and imply the postcondition with the negated guard; and STRENGTHENSPEC may “Only modify requires/ensures clauses” while preserving the original semantic intent (Appendix A, PDF pp. 13–14). The post-processing pipeline strips markdown code fences and language tags, validates brace matching, removes duplicate signatures, normalizes Unicode characters, and trims trailing whitespace and empty lines (Appendix B.3, PDF p. 15).

DIAGNOSEERROR uses two stages: pattern matching handles 84% of cases, while an LLM receives the full error context for the remaining 16% (“compound errors, ambiguous messages, and novel error patterns”) (Appendix B.4, PDF p. 15). The Stage 1 patterns map “postcondition might not hold” to spec_gap, “loop invariant might not be maintained” and “loop invariant might not hold on entry” to invariant_missing, “assertion might not hold” and “cannot prove termination” to body_error, and “unresolved identifier” and “type mismatch” / “expected” to type_error. Inference: a Verus port should measure its own category coverage before trusting deterministic routing; unmatched diagnostics must be treated as unknown rather than silently routed.

evidence and denominators

On the full benchmark of 178 examples, SKILLFORGE’s verification rate (VR) is 91.6% (163/178, Table 5) and equivalence rate 86.5%; its first-pass rate is 71.3% (127/178, Table 5). Section 4.2 says all baselines use GPT-5.5 “with identical iteration budgets (N=5) for fairness”, but Laurel and MCTS-Repair are budgeted by nodes (50) and rollouts (50) instead. ReAct-Verify reaches 82.0% VR and MCTS-Repair 84.3%; the strongest baseline is Proof2Silicon at 85.4% (an adapted prompt-repair version, not RL training, section 4.2). SKILLFORGE averages 1.8 iterations on successful cases. The 5.1 percentage-point VR–ER gap (91.6 − 86.5) indicates verified programs that differ semantically from the references (Table 2, PDF p. 8).

Difficulty matters: VR is 98.4% on 62 simple tasks, 93.0% on 71 medium tasks, and 77.8% on 45 hard tasks (Table 3, PDF p. 8). Removing DIAGNOSEERROR (random route) drops VR from 91.6% to 79.8% (−11.8 points); removing INFERSPEC drops it to 80.3% (−11.3); removing GENINVARIANT drops it to 83.7% (−7.9); removing the iterative loop leaves 71.3% (−20.3) (Table 4, PDF p. 8). The repair table reports success rates of 88.2% for DIAGNOSEERROR (51 invocations), 72.7% for REPAIRCODE (22), 75.0% for STRENGTHENSPEC (12), and 64.7% for GENINVARIANT (17) (Table 6, PDF p. 8).

Cost per example is 4.6K tokens, 2.8 verifier calls, and 14.2 seconds for SKILLFORGE, versus 8.9K/3.5/22.4 for ReAct-Verify and 14.2K/8.6/38.7 for MCTS-Repair (Table 8, PDF p. 9). These figures use GPT-5.5, Dafny 4.5.0, Z3 4.12.2, a 30-second verification timeout, and Python 3.11 (section 4.4, PDF p. 6; Table 8, PDF p. 9). Table 13 (Appendix G, PDF p. 18) reports 89.9% VR with Claude Opus-4.7 and 84.3% with Claude Sonnet-4.5.

Inference: the paper’s numbers are not fully self-consistent, so treat small differences with caution. (a) Table 3 rates correspond to 61 + 66 + 35 = 162 verified examples, not the 163 in Table 5. (b) Table 7 reports 76.5% repair success over 51 failures, but Table 5 implies 36 of the 51 first-attempt failures were repaired (70.6%), with 15 left as final failures. (c) Appendix C analyzes “36 examples where ReAct-Verify fails but SKILLFORGE succeeds”, yet ReAct-Verify’s 82.0% VR leaves only about 32 failures out of 178. (d) Table 6 invocation counts for repair skills (22, 12, 17) differ from the Table 7 category counts (19, 14, 13).

trust, limits, and threat to VL

Inference: the harness’s non-return of unverified code is a procedural soundness property, conditional on Dafny and Z3, the generated specification, and the verifier’s semantics; the paper itself calls the soundness “unconditional” (section 3.3). The authors report, in the Limitations section (PDF p. 9, after the Conclusion), a 178-example benchmark “limited in scale”, no evaluation of open-source models, a 5.1% VR–ER gap, GENINVARIANT as the lowest-success skill (64.7%), hand-crafted skill templates, and agentic baselines that “follow published methodologies adapted to Dafny; implementation differences may affect absolute numbers.” The benchmark descriptions were written by the authors rather than LLM-generated (section 4.1, PDF p. 5).

Inference: The threat to agent-written verified Rust is that a high verifier pass rate can hide a wrong contract, as the VR–ER gap demonstrates. VL should retain equivalence or reference checks, preserve bounded routing, and measure semantic alignment separately from proof success. What VL should not redo is the generic claim that verifier feedback helps; this paper already quantifies it (though the ablation was run on one benchmark and one main LLM backend). The open work is Verus-specific diagnosis, specification alignment, and behavior-preserving repair across Rust APIs.

techniques for the catalog

• atomic skill library: split specification, body, invariant, diagnosis, repair, and strengthening into independently checked skills
• deterministic error routing: map verifier categories to specialized repair skills
• bounded verification loop: use iteration caps, stagnation detection, and rollback to guarantee termination
• specification anchoring: forbid body synthesis from weakening the user’s contract
• equivalence verification: compare generated and reference preconditions, postconditions, and behavior Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Table 5 shows that 71.3% of programs are verified on the first attempt, and 83.1% converge within two iterations.”): read the whole paper text start to finish and checked every quotation, number, table value, section and PDF page reference, and technique step in this study against it; changed the PDF page numbers (most were off), the attribution of the state/rollback description (section 3.3 prose, not Algorithm 1), the “identical budget” wording, the Limitations section reference, and added Algorithm 1 details, Appendix F/G facts, baseline caveats, and a note on internal inconsistencies in the paper’s numbers (marked Inference); did not check the cited reference list, the Dafny prompt code in the appendices beyond the points cited, or the paper’s results by rerunning anything.

Last edited: 2026-10-17