# VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Agent skill learning and evolution, one of 16 directions in LLM agents and tool use.
- Builds on 26 of its 33 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Placed in

- LLM agents and tool use / [Agent skill learning and evolution](https://mlsanity.com/agents/agent-skill-learning-and-evolution/)
- Synthetic data and self-improvement for LLMs / [Self-evolving LLM agents](https://mlsanity.com/synth/self-evolving-llm-agents/)

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Learning to summarize from human feedback](https://mlsanity.com/paper/2009.01325/) (2020)
- [Do As I Can, Not As I Say: Grounding Language in Robotic Affordances](https://mlsanity.com/paper/2204.01691/) (2022)
- [Voyager: An Open-Ended Embodied Agent with Large Language Models](https://mlsanity.com/paper/2305.16291/) (2023)
- [Code as Policies: Language Model Programs for Embodied Control](https://mlsanity.com/paper/2209.07753/) (2022)
- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [Eureka: Human-Level Reward Design via Coding Large Language Models](https://mlsanity.com/paper/2310.12931/) (2023)
- [TextGrad: Automatic "Differentiation" via Text](https://mlsanity.com/paper/2406.07496/) (2024)
- [AutoSkill: Experience-Driven Lifelong Learning via Skill Self-Evolution](https://mlsanity.com/paper/2603.01145/) (2026)
- [TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks](https://mlsanity.com/paper/2401.12869/) (2024)
- [Exploring LLM-based Agents for Root Cause Analysis](https://mlsanity.com/paper/2403.04123/) (2024)
- [AutoManual: Constructing Instruction Manuals by LLM Agents via Interactive Environmental Learning](https://mlsanity.com/paper/2405.16247/) (2024)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools](https://mlsanity.com/paper/2404.11891/) (2024)
- [Deploying and Evaluating LLMs to Program Service Mobile Robots](https://mlsanity.com/paper/2311.11183/) (2023)
- [LLM-AutoDiff: Auto-Differentiate Any LLM Workflow](https://mlsanity.com/paper/2501.16673/) (2025)
- [LLM-based Robot Task Planning with Exceptional Handling for General Purpose Service Robots](https://mlsanity.com/paper/2405.15646/) (2024)
- [VerifyLLM: LLM-Based Pre-Execution Task Plan Verification for Robots](https://mlsanity.com/paper/2507.05118/) (2025)
- [Know Where You're Uncertain When Planning with Multimodal Foundation Models: A Formal Framework](https://mlsanity.com/paper/2411.01639/) (2024)
- [Fine-Tuning Language Models Using Formal Methods Feedback](https://mlsanity.com/paper/2310.18239/) (2023)
- [Multimodal Pretrained Models for Verifiable Sequential Decision-Making: Planning, Grounding, and Perception](https://mlsanity.com/paper/2308.05295/) (2023)
- [Robo-Instruct: Simulator-Augmented Instruction Alignment For Finetuning Code LLMs](https://mlsanity.com/paper/2405.20179/) (2024)
- [LAD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback](https://mlsanity.com/paper/2509.18384/) (2025)

## Built on by (most cited first, 3 of 3)

- [Recursive Self-Improvement in AI: From Bounded Self-Refinement to Autonomous Research Loops](https://mlsanity.com/paper/2607.07663/) (2026)
- [Autonomous Research Agents: A Survey of AI Scientists and the Verification Gap](https://mlsanity.com/paper/2608.05179/) (2026)
- [EMHO: EMbodied Agent Harness Optimization via Experience Traces](https://mlsanity.com/paper/2610.08432/) (2026)

## Abstract (arXiv)

Reusable robot skills are becoming the basic units through which embodied agents turn open-ended instructions into long-horizon physical behavior. We argue that, while foundation models have collapsed the cost of creating these skills, the cost of trusting them has not. Existing skill-evolution loops refine skills through execution feedback, unit tests, environment reward, or LLM self-critique, but these signals provide only trace-level evidence: they show that a skill worked on sampled executions, not that skill-induced plans satisfy temporal safety contracts under untested conditions. We introduce VASO, a framework for verification-guided self-evolution of LLM-generated robot skill contracts. In VASO, each skill is represented as a semantic contract with two coupled interfaces: a formal interface that aligns robot states, observations, and control commands with logical propositions for model checking, and a planner-facing interface that guides executable behavior generation. A model checker first filters logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications. When verification fails, VASO translates the counterexample trace into a textual gradient that updates the reusable skill contract while keeping foundation-model weights frozen. On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples, outperforming execution-feedback, prompt-optimization, and fine-tuning baselines. To our knowledge, VASO is the first framework that closes the loop between formal verification and self-evolving LLM-generated skills for physical AI agents: formal counterexamples become optimization feedback for reusable robot skill contracts, rather than merely verifying one-off plans, tuning planner prompts, or fine-tuning model weights.