让智能体技能可形式化验证，三步实现从声明到正式证明的跨越。
Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof
- 通过抽象解释分析脚本侧能力，确保行为符合预期。
- 用细化类型系统拒绝能力不符的工具调用，防止越权。
- 结合SMT模型检测，自动验证技能在运行时边界内的正确性。
本文补全了前作提出的四层智能体技能验证体系中的顶层。我们为技能行为给出了精确语义，刻画了大模型驱动运行时中脚本侧（确定性）与大模型侧（非确定性）的交互方式，将验证问题形式化为能力包含关系。提出三种可组合的方法：(1) 基于小效应格的抽象解释，对脚本侧进行声学的能力包含静态分析；(2) 工具调用封装的细化类型系统，机械排除静态推断能力不在声明集中的调用；(3) 在父论文双条件正确性标准下，基于SMT的有界模型检测，边界设置使得任何符合运行时事务缓冲周期的反例都能以具体轨迹呈现。证明三者组合在除大模型自主拒绝行为外，完全覆盖父论文威胁模型，该残余风险由父论文运行时双条件在会话边界捕获。方法复用现有成熟工具（Z3、Semgrep、CodeQL、细化类型检查器、机械化证明助手），无需新构建；证明携带的产物扩展了现有SKILL.md规范。所有方法连同打包生产器与重检器已作为零依赖JavaScript模块开源发布于enclawed框架（https://github.com/metereconsulting/enclawed），含53个单元测试及端到端命令行演示样例技能。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。