代理技能形式化验证方法：三层通向可机械检查的能力-包含证明

伴随论文介绍了关于代理技能清单（未验证、已声明、已测试、形式化）的四层验证格局，留下了最高层的野心。本文填补了这一空白。我们给出忠实于 LLM 驱动运行时（通过 LLM 端非确定性实现，通过脚本端确定性）如何消费技能的技能行为语义， 将验证问题表述为该语义上的能力-包含属性，并提出三种可组合的方法，将技能从已声明或已测试提升至形式化：（1）通过抽象解释对脚本端的 sound 静态能力-包含分析，基于小型效应格局；（2）针对工具调用信封的细化类型系统，机械地拒绝其静态推断能力不在清单声明集合中的任何调用；（3）基于父论文提出的双向正确性准则进行 SMT 边界模型检查，界限 chosen such 使任何符合运行时事务缓冲区视野的反例都呈现为具体轨迹。我们证明，三层方法组合在覆盖父论文威胁模型方面是 sound 的，除去一个剩余（LLM 自由拒绝行动），该剩余在会话边界被父论文的双向正确性捕获。该方法重用现有的成熟工具（Z3、Semgrep、CodeQL、细化类型检查器、机械化证明助手），而非要求运营商构建新工具， proof-carrying artifact extends 现有的 SKILL.md 约定。所有三种方法 plus 捆绑生产者和 re-checker 以零依赖 JavaScript 模块形式发布于开源 enclawed 框架中（https://github.com/metereconsulting/enclawed；项目页面 https://www.enclawed.com/），包含 53 个单元测试和针对示例技能的端到端 CLI 演示。