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

• URL: http://arxiv.org/abs/2606.05395v1
• Date: Wed, 03 Jun 2026 20:02:35 GMT
• Title: VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents
• Abstract summary: We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
• Score: 57.240036084348354
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
  We introduce SKILLFORGE, a framework that decomposes formal code synthesis into a library of atomic, reusable skills.<n>A verification-driven harness orchestrates these skills.<n>On a curated benchmark of natural language to Dafny specification pairs, SKILLFORGE substantially outperforms both state-of-the-art agentic approaches.
  arXiv  Detail & Related papers  (2026-08-30T15:15:00Z)
• Self-Evolving Embodied Agents via Skill-Harness Evolution [53.307052568223945]
  Embodied agents are increasingly built as systems around foundation models.<n>While supervised fine-tuning and reinforcement learning can adapt agents to new environments, they require additional data, rewards, and training runs.<n>We propose SHAPER, a self-evolving framework for train-free embodied adaptation that keeps model parameters frozen.
  arXiv  Detail & Related papers  (2026-08-11T18:55:58Z)
• AEVAL: From Anecdotal to Deterministic Testing for Agentic Skill Workflows [1.6785141970297952]
  AEVAL (Agentic Evaluation) is a CI-integrated framework that replaces this practice with a deterministic, reproducible test pipeline for agentic skills.<n>Every skill change triggers a test event: the skill runs against a developer declared evaluation contract inside an automated executor.<n>A key ingredient is a structural separation between executor and grader, preventing a subtle but pervasive failure mode.
  arXiv  Detail & Related papers  (2026-07-16T21:33:05Z)
• Beyond the Syntax: Do Security Experts Trust LLMs for NIDS Rule Engineering? [70.17374586573033]
  This paper presents a human-centered investigation into Large Language Models (LLMs)-based NIDS rule engineering.<n>Our evaluation reveals a syntax-semantics paradox: although LLMs generate syntactically correct rules, experts find them only partially deployable.<n>While large-scale models consistently produce syntactically valid rules, small models are largely ineffective for IDS rule generation.
  arXiv  Detail & Related papers  (2026-07-07T07:09:56Z)
• Declarative Skills for AI Agents in Knowledge-Grounded Tool-Use Workflows [1.9573380763700712]
  We study orchestration mechanisms for tool-using AI agents in realistic customer-service errors over an unstructured knowledge base.<n>We compare (i) a DeclarativeAgent that reads three domain-specific skill files at inference time and decides its own control flow, (ii) an ImperativeAgent based on a programmatic state machine with explicit phases, and (iii) an unscaffolded baseline agent modeled after the $$-Knowledge benchmark agent.
  arXiv  Detail & Related papers  (2026-06-05T05:38:51Z)
• Contractual Skills: A GovernSpec Design Framework for Enterprise AI Agents [8.419155861590548]
  This paper proposes contractual skills, a GovernSpec-inspired design framework for organizing SKILL.md files as readable task contracts.<n>The framework clarifies the boundary between contractual skills, GovernSpec YAML contracts, Model Context Protocol (MCP) surfaces, tool adapters, runtime guardrails, tracing, and evaluation systems.
  arXiv  Detail & Related papers  (2026-05-21T15:40:05Z)
• Harnessing LLM Agents with Skill Programs [58.356514745548026]
  We introduce HASP, a new framework that upgrades skills into executable Program Functions (PFs)<n>PFs act as executable guardrails that activate on failure-prone states and modify the next action or inject corrective context.<n> HASP drives substantial gains compared to both training-free and training-based methods on web-search, math reasoning, and coding tasks.
  arXiv  Detail & Related papers  (2026-05-18T01:35:11Z)
• Skill-R1: Agent Skill Evolution via Reinforcement Learning [84.35984979949502]
  Skill-R1 is a reinforcement learning framework for instance-level recurrent skill optimization from verifiable rewards.<n>It preserves black-box compatibility with both open- and closed-source models while making adaptation substantially cheaper than model-level updates.
  arXiv  Detail & Related papers  (2026-05-10T06:19:15Z)
• SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
  Self-evolving agent frameworks provide no formal guarantees of safety or correctness.<n>We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility.<n>We present SEVerA, a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning.
  arXiv  Detail & Related papers  (2026-03-26T07:32:20Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  We present DrillAgent, an agentic framework that reformulates PoV generation as an iterative hypothesis-verification-refinement process.<n>We evaluate DrillAgent on SEC-bench, a large-scale benchmark of real-world C/C++ vulnerabilities.
  arXiv  Detail & Related papers  (2026-02-14T03:17:27Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations, and (iii) semantic drift as intent is reinterpreted across agent handoffs.<n>We propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs.
  arXiv  Detail & Related papers  (2026-01-27T16:10:23Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.