Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof

• URL: http://arxiv.org/abs/2605.23951v1
• Date: Sat, 09 May 2026 19:27:38 GMT
• Title: Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof
• Abstract summary: We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime.<n>We present three composable methods that together raise a skill from declared or tested to formal.<n>All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The companion paper introduced a four-level verification lattice on agent-skill manifests (unverified, declared, tested, formal) and left the top level aspirational. This paper closes that gap. We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime (a deterministic script-side reachable through a non-deterministic LLM-side), state the verification problem as a capability-containment property over that semantics, and present three composable methods that together raise a skill from declared or tested to formal: (1) sound static capability-containment analysis of the script-side via abstract interpretation over a small effect lattice; (2) a refinement type system for tool-call envelopes that mechanically rejects any call whose statically-inferred capability is not in the manifest's declared set; (3) SMT-bounded model checking against the parent paper's biconditional correctness criterion, with the bound chosen so any counter-example fitting the runtime's transaction-buffer horizon is exhibited as a concrete trace. We prove the three layers composed soundly cover the parent paper's threat model modulo a single residual (the LLM's freedom to refuse to act) that the parent paper's runtime biconditional catches at session boundary. The methods reuse existing well-engineered tools (Z3, Semgrep, CodeQL, refinement-type checkers, mechanised proof assistants) rather than asking operators to build new ones, and the proof-carrying artifact extends the existing SKILL.md convention. All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework (https://github.com/metereconsulting/enclawed; project page https://www.enclawed.com/), with 53 unit tests and an end-to-end CLI demo on a sample skill.

Related papers

• Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
  General-purpose text embeddings are widely deployed for such tasks, but broad semantic similarity can place semantically similar yet task-distinct examples.<n>We introduce Prototype-Guided Contrastive Learning (PGCL), a prototype-guided geometric regularization module built on top of frozen text embeddings.
  arXiv  Detail & Related papers  (2026-08-15T13:19:25Z)
• PluginEval: A Diagnostic Benchmark for Fine-Grained Error Attribution in Function Calling [11.1017602726296]
  Large Language Models increasingly operate as autonomous agents.<n>Current benchmarks face three structural limitations.<n>Eval is a benchmark constructed through a two-stage framework.
  arXiv  Detail & Related papers  (2026-08-09T13:25:54Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  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.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• AgentSecBench: Measuring Prompt Injection, Privacy Leakage, and Tool-Use Integrity in LLM Agents [0.2864713389096699]
  We introduce AgentSecBench as an empirical instantiation of a formal security framework for this problem.<n>It defines three games-instruction-integrity, retrieval-confidentiality, and capability-integrity-under a common notion of intent-to-execution noninterference with permitted leakage.<n>It represents an application policy as a projection onto authorized observations and capabilities, distinguishes prompt annotations from enforcing projections, and measures both adversarial advantage and whether a defense closes the relevant model-visible channel before generation.
  arXiv  Detail & Related papers  (2026-05-25T18:53:22Z)
• PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
  PRIMA operates as coordinated multi-agent research systems over multi-hour runs.<n>Main contributions are three operational patterns for surviving failure modes.<n>A Graph Isomorphism case study grounds the architectural claims in a generated artifact.
  arXiv  Detail & Related papers  (2026-05-23T23:27:46Z)
• Agentic Model Checking [12.832868209928039]
  We propose a paradigm that couples LLM agents with a bounded model checking backend.<n>We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust.
  arXiv  Detail & Related papers  (2026-05-20T17:25:52Z)
• Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
  We argue that securing LLM agents requires defining an end-to-end correctness property that specifies when an agent's execution faithfully reflects the user's intent.<n>We observe that LLM agents are structurally analogous to compilers, where security violations correspond to mis-executions that do not preserve user intent.<n>We derive four integrity properties that must hold simultaneously: emphTool Integrity, emphInstruction Integrity, emphJudgment Integrity, and emphData Flow Integrity.
  arXiv  Detail & Related papers  (2026-05-16T12:53:31Z)
• Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
  We present a framework for verifying the deterministic structured computations surrounding a large language model.<n>We extend a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines.
  arXiv  Detail & Related papers  (2026-05-13T12:01:41Z)
• Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes [0.0]
  We argue that a skill is emphuntrusted code until it is verified.<n>Without skill verification, a human-in-the-loop gate must fire on every irreversible call.<n>We give a trust schema that includes an explicit verification level on every skill manifest.
  arXiv  Detail & Related papers  (2026-05-01T05:53:05Z)
• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  Large Language Models (LLMs) have evolved from simple text generators into complex software systems that integrate retrieval augmentation, tool invocation, and multi-turn interactions.<n>Their inherent non-determinism, dynamism, and context dependence pose fundamental challenges for quality assurance.<n>This paper decomposes LLM applications into a three-layer architecture: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, and textbftextitLLM Inference Core.
  arXiv  Detail & Related papers  (2025-08-28T13:00:28Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)

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.