# VeriSkill: A Self-Evolution Framework for Program Verification Skills

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

## 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 13 of its 30 references that are in the map.
- First posted on arXiv 30 Jul 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, 13 of 13)

- [SkillsBench: Benchmarking How Well Agent Skills Work Across Diverse Tasks](https://mlsanity.com/paper/2602.12670/) (2026)
- [Trace2Skill: Distill Trajectory-Local Lessons into Transferable Agent Skills](https://mlsanity.com/paper/2603.25158/) (2026)
- [CoEvoSkills: Self-Evolving Agent Skills via Co-Evolutionary Verification](https://mlsanity.com/paper/2604.01687/) (2026)
- [AutoSkill: Experience-Driven Lifelong Learning via Skill Self-Evolution](https://mlsanity.com/paper/2603.01145/) (2026)
- [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)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [SkillOpt-Lite: Better and Faster Agent Self-evolution via One Line of Vibe](https://mlsanity.com/paper/2607.03451/) (2026)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Automated Patch Assessment for Program Repair at Scale](https://mlsanity.com/paper/1909.13694/) (2019)
- [A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs](https://mlsanity.com/paper/2512.24594/) (2025)
- [AxDafny: Agentic Verified Code Generation in Dafny](https://mlsanity.com/paper/2606.32007/) (2026)

## Abstract (arXiv)

Automating program verification with LLM agents requires generating specifications, annotations, auxiliary lemmas, and tool invocations, all of which depend on reusable skills. A natural remedy is skill self-evolution: distilling skills from trajectories and refining them through feedback. However, existing evolution methods struggle with program verification tasks because they cannot reliably identify skill-specific failures or extract actionable signals from opaque verifier feedback. In this paper, we propose VeriSkill, a self-evolution framework built for program verification. It attributes verification failures to skill deficiencies, distills diagnostic signatures into reusable lessons, and iteratively refines candidate skills, admitting only revisions that improve verification performance while preserving program semantics. Experiments show that VeriSkill consistently outperforms all baselines across multiple verification tools, agent frameworks, and LLM backends.