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

arXiv: https://arxiv.org/abs/2608.29841 · HTML: https://mlsanity.com/paper/2608.29841/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent skill learning and evolution, one of 16 directions in LLM agents and tool use.
- Builds on 23 of its 71 references that are in the map.
- First posted on arXiv 30 Aug 2026.

## Placed in

- LLM agents and tool use / [Agent skill learning and evolution](https://mlsanity.com/agents/agent-skill-learning-and-evolution/)

## Builds on (most cited first, 23 of 23)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [Agentless: Demystifying LLM-based Software Engineering Agents](https://mlsanity.com/paper/2407.01489/) (2024)
- [Planning with Large Language Models for Code Generation](https://mlsanity.com/paper/2303.05510/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Memento-Skills: Let Agents Design Agents](https://mlsanity.com/paper/2603.18743/) (2026)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Large Language Models Based Automatic Synthesis of Software Specifications](https://mlsanity.com/paper/2304.09181/) (2023)
- [Large Language Models for Code Generation: The Practitioners Perspective](https://mlsanity.com/paper/2501.16998/) (2025)
- [Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation](https://mlsanity.com/paper/2311.10483/) (2023)
- [Dafny as Verification-Aware Intermediate Language for Code Generation](https://mlsanity.com/paper/2501.06283/) (2025)
- [Adaptive Proof Refinement with LLM-Guided Strategy Selection](https://mlsanity.com/paper/2510.25103/) (2025)
- [Chain-Aware Encoding for Microservice Trace Anomaly Detection](https://mlsanity.com/paper/2607.10156/) (2026)
- [Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation](https://mlsanity.com/paper/2601.19747/) (2026)
- [Cross-Asset Risk Management: Integrating LLMs for Real-Time Monitoring of Equity, Fixed Income, and Currency Markets](https://mlsanity.com/paper/2504.04292/) (2025)
- [Dynamic Hedging Strategies in Derivatives Markets with LLM-Driven Sentiment and News Analytics](https://mlsanity.com/paper/2504.04295/) (2025)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)

## Abstract (arXiv)

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.