PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Jinbo Su

arXiv:2608.29841v1cs.CLcs.PL

TL;DR

Generating formally verified programs from natural language is difficult because existing methods either lack repair after verification failure or rely on opaque, non-deterministic reasoning. SKILLFORGE decomposes synthesis into atomic skills and deterministically routes structured Dafny-verifier feedback to targeted repairs, achieving higher verification performance with fewer tokens and lower latency.

  • Problem

    Existing approaches either provide no diagnosis or repair after one-shot generation fails, or use non-deterministic and opaque open-ended reasoning for formal code synthesis.

  • Method

    SKILLFORGE uses six contract-defined skills orchestrated by a verification-driven harness that categorizes verifier errors and deterministically routes candidates to targeted repairs.

  • Results

    SKILLFORGE substantially outperforms agentic and traditional iterative baselines, achieving a 91.6% verification rate on a 178-example benchmark.

  • Takeaways & Limitations

    When a perfect oracle provides categorizable error output, structured skill decomposition with deterministic routing offers a transparent, modular, formally sound, and efficient alternative to open-ended agentic systems.

  • Takeaways & Limitations

    The benchmark has 178 examples, the skill library is Dafny-specific, open-source-model performance is unexplored, and complex quantifier-heavy loops remain a failure mode.

Abstract

from arXiv · show

Generating formally verified programs from natural language remains challenging: existing approaches either produce code in a single pass without recourse when verification fails, or rely on open-ended agentic reasoning that is non-deterministic and opaque. We introduce SKILLFORGE, a framework that decomposes formal code synthesis into a library of atomic, reusable skills, each targeting a specific subtask such as specification inference, body synthesis, invariant generation, error diagnosis, or targeted repair, and defined by a prompt template, tool binding, and decidable success criterion. A verification-driven harness orchestrates these skills: it submits candidates to the Dafny verifier, diagnoses failures into structured categories, deterministically routes to the appropriate repair skill, and iterates until formal correctness is proved or a budget is exhausted. On a curated benchmark of natural language to Dafny specification pairs, SKILLFORGE substantially outperforms both state-of-the-art agentic approaches (including ReAct-style agents, MCTS-based repair, and RL-guided verification) and traditional iterative baselines, while requiring fewer tokens and lower latency. Ablation studies confirm that every skill contributes measurably, and the harness converges rapidly with the majority of programs verified on the first attempt.

1 Introduction

SKILLFORGE addresses the difficulty of generating verification-grade Dafny programs by decomposing synthesis into atomic skills and deterministically routing verifier feedback to targeted repairs. On a 178-example benchmark, it achieves a 91.6% verification rate while outperforming agentic baselines.

  • Formal verification requires implementations, tight specifications, and auxiliary annotations that jointly satisfy the verifier.
  • One-shot generation lacks diagnosis and repair when verification fails, while naive iterative repair conflates distinct failure types.
  • Agent-based and tree-search approaches introduce non-determinism, opacity, unbounded computation, or poorly targeted exploration for categorized verification errors.
  • SKILLFORGE decomposes synthesis into atomic skills and uses a harness with deterministic routing, bounded iteration, and observable execution.
  • The verifier’s structured errors are categorized to select the next repair skill, replacing open-ended action selection with an auditable routing decision.
  • 91.6% verification rate was achieved on a 178-example benchmark, outperforming four state-of-the-art agentic baselines.

2 Related Work

Related work spans LLM-based specification and Dafny synthesis, automated program repair, loop-invariant generation, agentic code generation, and tree-search verification. SKILLFORGE differentiates itself through deterministic skill selection rather than open-ended reasoning or candidate exploration.

  • LLM-based work applies language models to specification synthesis, Dafny generation, benchmark construction, and proof-tactic selection.
  • Traditional and neural automated program repair rely on tests or generated patches, whereas Dafny verification provides pass/fail judgments over all inputs.
  • Prior loop-invariant methods rank, filter, or symbolically validate candidate invariants using LLMs and formal analysis.
  • Agentic code-generation systems interleave reasoning, tool calls, or executable actions, while simpler non-agentic workflows can achieve comparable results at lower cost.
  • Tree-search and verification-guided methods explore multiple candidates but face combinatorial growth; SKILLFORGE selects one repair skill from structured error categories.
  • Compositional skill systems motivate reusable skill libraries and skill combinations, including frameworks that autonomously grow task-specific skills.

3 Methodology

SKILLFORGE models Dafny synthesis as sequential, contract-defined skill invocations orchestrated by a verification-driven harness. The harness diagnoses failures, applies targeted repairs, tracks progress, and guarantees that returned programs are verified.

  • 3.1 Problem Formulation: The goal is a Dafny program that compiles, satisfies its Hoare triple, and is semantically equivalent to a reference implementation.
  • 3.2 Skill Library: Each skill is defined by a prompt template, tool binding, and decidable success criterion.
  • 3.2 Skill Library: INFERSPEC extracts structured metadata from natural language, while SYNTHBODY generates an executable body conditioned on the specification scaffold.
  • 3.2 Skill Library: Specification anchoring forbids modifying the specification, preventing models from weakening postconditions to make verification trivial.
  • 3.2 Skill Library: GENINVARIANT generates entry-valid, inductive invariants whose combination with the negated guard implies the postcondition.
  • 3.2 Skill Library: DIAGNOSEERROR classifies failures using regex for common cases and LLM reasoning for ambiguous cases, returning a category, line, and suggestion.
  • 3.2 Skill Library: REPAIRCODE makes minimal edits at the identified failure site to preserve the algorithmic approach and support convergence.
  • 3.3 Verification-Driven Harness: The harness composes initial synthesis, error-conditioned routing, iterative state tracking, rollback, bounded termination, and stagnation checks.

4 Experimental Setup

The evaluation uses a curated, difficulty-stratified benchmark and compares SKILLFORGE with traditional iterative, agentic, and tree-search baselines under matched compute settings. Outcomes include verification, semantic equivalence, iteration efficiency, and first-pass success.

  • Benchmark: The benchmark contains 178 natural-language–Dafny pairs curated from the Dafny Standard Library, DafnyBench, and open-source verification projects.
  • Benchmark: Authors wrote all natural-language descriptions and stratified examples into Simple, Medium, and Hard difficulty levels.
  • Baselines: Traditional baselines include one-shot, structured one-shot, naive repair, and chain-of-thought plus repair prompting.
  • Baselines: Agentic baselines include ReAct-Verify and CodeAct-Dafny, while verification-guided baselines include MCTS-Repair, Laurel, Clover, and Proof2Silicon.
  • Implementation: All baselines use GPT-5.5 with identical five-iteration budgets for fairness.
  • Metrics: Evaluation metrics are Verification Rate, Equivalence Rate, Average Iterations, and First-Pass Rate.
  • Implementation: Experiments use GPT-5.5 as the primary backend, Claude models for comparison, Dafny 4.5.0 with Z3 4.12.2, a five-iteration maximum, and 30-second verification timeouts.

5 Results

SKILLFORGE achieves the strongest verification results while using targeted, deterministic repair and converging rapidly. Its gains are largest on difficult invariant-heavy tasks, and ablations identify verification-in-the-loop, diagnosis, specification inference, and invariant generation as key contributors.

  • Main Results: 91.6% verification rate on 178 examples, exceeding Proof2Silicon by 6.2 percentage points and CoT + Repair by 14.1 pp.
  • Results by Difficulty: SKILLFORGE’s advantage increases with difficulty, reaching 77.8% versus 64.4% on Hard tasks, a 13.4 pp improvement over the best agentic baseline.On Medium tasks, it leads MCTS-Repair by 9.9 pp, 93.0% versus 83.1%.
  • Skill-Level Ablation: GENINVARIANT reduces verification rate by 7.9 pp overall and 22.2 pp on Hard tasks, identifying invariant synthesis as a distinct bottleneck.Invariant failures have the lowest repair rate at 69.2%, while DIAGNOSEERROR reaches 88.2%.
  • Skill-Level Ablation: Removing the iterative loop reduces verification rate by 20.3 pp, the largest ablation effect, while DIAGNOSEERROR reduces it by 11.8 pp.The diagnosis ablation reaches 79.8%, comparable to agentic baselines.
  • Convergence: 71.3% of programs verify on the first attempt, 83.1% converge within two iterations, and only 2.8% require four or more rounds.SKILLFORGE averages 1.8 iterations, compared with 2.5 for ReAct-Verify and 2.8 for CodeAct-Dafny.
  • Cost and Efficiency: SKILLFORGE uses 48% fewer tokens than ReAct-Verify and 68% fewer than MCTS-Repair while achieving higher verification rates.MCTS-Repair invokes the verifier 8.6 times per example versus 2.8 for SKILLFORGE.

6 Conclusion

SKILLFORGE synthesizes formally verified Dafny programs from natural language by decomposing the task into six atomic skills and routing them through verification-driven orchestration. The framework substantially outperforms agentic and traditional iterative baselines while using fewer tokens and lower latency.

  • 6 Conclusion: SKILLFORGE decomposes formally verified Dafny synthesis into six atomic skills orchestrated through verification-driven routing.The framework is designed for natural-language-to-Dafny synthesis and uses skill decomposition rather than a monolithic generation process.
  • 6 Conclusion: The harness provides transparency, modularity, formal soundness, and efficiency as an alternative to agent-based systems.Its routing is structured around verification feedback rather than open-ended agent behavior.
  • 6 Conclusion: SKILLFORGE substantially outperforms agentic approaches and traditional iterative baselines while consuming fewer tokens and achieving lower latency.The conclusion frames this result as evidence for skill-based harness engineering in domains with structured oracle feedback.

Limitations

The paper’s scope is constrained by a small, Dafny-specific benchmark, limited model coverage, semantic mismatches, hand-crafted skills, and possible baseline implementation differences. Its templates and techniques therefore do not yet establish broad transferability or complete semantic alignment.

  • Limitations: The benchmark contains 178 examples and is limited in scale.The authors describe it as comparable to existing formal verification benchmarks but still small.
  • Limitations: The skill library is Dafny-specific, and transfer to Lean 4 or Coq requires new implementations.The limitation concerns portability across formal-verification languages.
  • Limitations: Primary experiments use GPT-5.5 and Claude Opus-4.7, while performance on open-source models remains unexplored.The reported evaluation does not establish how the framework behaves across open-source model families.
  • Limitations: A 5.1% VR–ER gap indicates that some verified programs deviate semantically from references.The paper identifies semantic alignment as distinct from verification success.
  • Limitations: GENINVARIANT succeeds at 64.7%, with complex quantifier-heavy loops remaining the primary failure mode.The authors identify this as a target for future improvement through specialized training or more sophisticated invariant templates.
  • Limitations: Skill templates are hand-crafted, and automatic refinement is left for future work.The current library does not automatically improve its own templates.
  • Limitations: Agentic baselines adapt published methodologies to Dafny, so implementation differences may affect absolute numbers.This caveat limits direct interpretation of the reported baseline comparisons.

B.2 Agentic Baseline Implementation Details

The baseline implementations compare bounded agentic and tree-search systems under explicit tool, rollout, beam, depth, and cycle configurations. The system also specifies modular skill interfaces, post-processing, and a two-stage error-classification procedure.

  • B.2 Agentic Baseline Implementation Details: ReAct-Verify uses verify, compile, and targeted edit tools with a maximum of five Thought-Action-Observation cycles.Its prompt includes a Dafny reference and an error interpretation guide.
  • B.2 Agentic Baseline Implementation Details: CodeAct-Dafny executes Python actions in a sandbox with Dafny verification, compilation, file I/O, and regex/AST utilities.The configuration permits at most five code-execution rounds, with average code actions of 12 lines.
  • B.2 Agentic Baseline Implementation Details: MCTS-Repair uses UCB1 selection with c = 2, 50 rollouts per example, five repair actions, and verification-based rewards.The available actions include invariant addition, body modification, precondition addition, postcondition strengthening, and decreases-clause addition.
  • B.2 Agentic Baseline Implementation Details: Laurel uses verification at each search node with beam width 3, maximum depth 10, and 50 explored nodes.Branches that increase verification errors are pruned, and the first verified complete program is returned.
  • B.2 Agentic Baseline Implementation Details: Each skill builds a prompt, invokes the language model, parses its output, checks success, and returns a SkillResult.The interface exposes abstract methods for prompt construction and success checking.
  • B.2 Agentic Baseline Implementation Details: Post-processing strips code fences, validates braces, removes duplicate signatures, normalizes Unicode, and trims trailing whitespace.These steps standardize generated outputs before subsequent handling.
  • B.2 Agentic Baseline Implementation Details: Error classification uses pattern matching for 84% of cases and LLM reasoning for the remaining 16%.The second stage handles compound, ambiguous, and novel error patterns.

C Agentic Baseline Failure Analysis

The failure analysis examines 36 cases where ReAct-Verify fails but SKILLFORGE succeeds, highlighting misdirected repairs and search expansion as dominant failure patterns. These examples connect baseline weaknesses to structured routing and difficulty-sensitive repair requirements.

  • C Agentic Baseline Failure Analysis: 36 examples are analyzed where ReAct-Verify fails but SKILLFORGE succeeds, revealing three dominant failure patterns.The analysis is summarized in Table 10.
  • C Agentic Baseline Failure Analysis: ReAct-Verify misdirects repair by modifying the body for a missing precondition, then exhausts its budget after reverting changes and introducing a typo.The absolute-value example reaches turn 5 without verification.
  • C Agentic Baseline Failure Analysis: On 45 Hard examples, MCTS-Repair’s branching factor limits search to rarely beyond depth 3 under 50 rollouts and five actions per node.This depth is insufficient when problems require two or more specific invariants simultaneously.
  • C Agentic Baseline Failure Analysis: MCTS-Repair reaches a verified program in 0.4 average rollouts per Hard example versus 3.2 per Simple example.The comparison quantifies the difficulty-sensitive collapse of search effectiveness.

D Extended Case Studies

The case studies show SKILLFORGE using verifier feedback to select narrowly targeted repairs, often reaching verified programs within two or three iterations. Failures remain on inductive proofs whose bodies require reasoning beyond the model’s capabilities.

  • Specification strengthening: 2 iterations verify the multiplication example after STRENGTHENSPEC adds the missing postcondition, while ReAct-Verify takes 3 turns and modifies the body unnecessarily.The harness diagnoses the missing ensures clause and applies a specification repair rather than changing correct implementation code.
  • Loop invariant generation: 2 iterations verify factorial after GENINVARIANT adds bounds, a functional invariant, and a termination measure.The initial loop body is correct, but verification fails because invariants are absent.
  • Simple predicates: First-pass success is reliable for simple single-clause predicates, with INFERSPEC correctly identifying the predicate construct.The maximum predicate example requires no repair.
  • Termination repair: 2 iterations verify recursive summation after REPAIRCODE adds the missing decreases clause classified as a body annotation error.The recursive body is correct, but termination cannot be proved without the measure.
  • Iterative repair: 3 iterations verify maximum-finding after iterative invariant generation first adds bounds and then relates max to previously seen elements.The example demonstrates progressive refinement from specific verifier feedback.
  • Failure cases: 5 iterations fail on the reverse-twice lemma because the model cannot synthesize an inductive proof body using sequence axioms.Agentic baselines also fail, indicating a limitation shared across evaluated methods rather than a distinctive harness failure.

E Benchmark Details

The benchmark combines curated Dafny examples from standard materials, DafnyBench, and open-source projects, spanning simple predicates through invariant-heavy and inductive-proof tasks. Evaluation checks interface, specification, and behavioral equivalence, while results examine model dependence, skill usage, convergence, and domain scope.

  • Data sources: 178 examples comprise 42 Dafny Standard Library cases, 86 DafnyBench cases, and 50 self-contained open-source project cases.Open-source examples compile with Dafny 4.5.0 and cover diverse specification patterns.
  • Difficulty classification: Simple tasks exclude loops and recursion, Medium tasks allow obvious termination or quantified specifications, and Hard tasks require invariants, non-trivial termination measures, or lemma proofs.These criteria define increasing verification difficulty by annotation and proof demands.
  • Evaluation pipeline: Semantic equivalence is evaluated through interface matching, specification equivalence, and behavioral equivalence under shared preconditions.The pipeline compares signatures, logically equivalent contracts, and outputs for all inputs satisfying the precondition.
  • Multi-model comparison: 91.6% verification is achieved with GPT-5.5, compared with 89.9% for Claude Opus-4.7 and 84.3% for Sonnet-4.5 under the full harness.The model gap is driven primarily by GENINVARIANT success, identifying invariant synthesis as the most capability-sensitive skill.
  • Scope and generalizability: The harness is best suited to domains with finite error taxonomies and perfect oracles, whereas agentic methods retain advantages when success criteria are ambiguous.The authors frame this as a scope boundary rather than a general indictment of agentic approaches.
  • Convergence and compute: Diminishing returns appear beyond 2 iterations for most examples, and structured test-time investment outperforms unstructured scaling with less compute.The comparison is made against MCTS-Repair and Proof2Silicon.
  • Skill utilization: 15 of 17 GENINVARIANT invocations occur on Hard tasks, while only 3 of 62 Simple tasks require repair.STRENGTHENSPEC is most common on Medium tasks, where specifications are non-trivial but expressible.
Loading 2608.29841v1…