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.

翻译：伴生论文提出了关于智能体技能清单的四级验证格（未验证、已声明、已测试、形式化），并将最高层级设定为理想目标。本文填补了这一空白。我们为技能行为给出了精确语义，该语义忠实反映了LLM驱动运行时对技能的消费方式（确定性脚本侧通过非确定性LLM侧可达），将验证问题定义为该语义上的能力包含属性，并提出了三种可组合方法，共同将技能从"已声明"或"已测试"层级提升至"形式化"层级：(1) 通过小效应格上的抽象解释，对脚本侧进行可靠静态能力包含分析；(2) 为工具调用封装设计精炼类型系统，能够机械拒绝任何静态推断能力不在清单声明集合中的调用；(3) 针对原论文的双条件正确性准则执行SMT有界模型检验，其有界范围确保任何符合运行时事务缓冲区视界的反例均能以具体迹形式呈现。我们证明这三层组合方法能够可靠覆盖原论文的威胁模型，仅余单个残余项（LLM拒绝行动的自主权），该残余项由原论文的运行时双条件机制在会话边界处捕获。这些方法复用现有成熟工程工具（Z3、Semgrep、CodeQL、精炼类型检查器、机械化证明助手），无需运维人员构建新工具，且携带证明的制品扩展了现有SKILL.md约定。三种方法及其打包生产与再检验组件均以零依赖JavaScript模块形式发布在开源enclawed框架中（https://github.com/metereconsulting/enclawed；项目页面https://www.enclawed.com/），包含53项单元测试及针对样本技能的端到端命令行演示。