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

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

## Key facts

- Cited by 1 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 6 of its 67 references that are in the map.
- First posted on arXiv 9 May 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, 6 of 6)

- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [SmoothLLM: Defending Large Language Models Against Jailbreaking Attacks](https://mlsanity.com/paper/2310.03684/) (2023)
- [AgentHarm: A Benchmark for Measuring Harmfulness of LLM Agents](https://mlsanity.com/paper/2410.09024/) (2024)
- [AgentPoison: Red-teaming LLM Agents via Poisoning Memory or Knowledge Bases](https://mlsanity.com/paper/2407.12784/) (2024)
- [GenAI Against Humanity: Nefarious Applications of Generative Artificial Intelligence and Large Language Models](https://mlsanity.com/paper/2310.00737/) (2023)
- [Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes](https://mlsanity.com/paper/2605.00424/) (2026)

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

- [Attested Tool-Server Admission: A Security Extension to the Model Context Protocol](https://mlsanity.com/paper/2605.24248/) (2026)

## Abstract (arXiv)

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.