SkillSpec 用意图掩码把技能正确性变成规格推理：515 个真实技能中确认 763 个缺陷，代码节点精度 67.1%

论文把智能体技能的正确性重新表述为“声明意图”与“编码行为”之间的一致性（规格一致性）问题，并借用 Hoare 三元组把技能拆成操作单元，为每个单元写出前置/后置条件式的文本谓词。 此前对技能的研究集中在基准评测、能力增强与安全攻击，非恶意缺陷很少被系统研究；该工作把经典 Hoare 推理从代码扩展到自然语言指令与异构资源混合的技能工件。 论文给出形式化定义（ExpectSpec 来自完整声明意图，FactSpec 来自被掩码意图下的实现），并以音频拼接操作为例说明未声明的副作用如何被暴露；作者明确说明这是文本谓词而非机器可检验的证明系统。

SkillSpec 构建统一图表示：把 SKILL.md 重建为带 contain 与 dependency 边的工作流 DAG，把脚本经 Tree-sitter 解析为语言无关 IR 并建调用图，再通过意图—实现绑定把工作流单元与代码节点双向映射。 相比 LLM 智能体常用的 grep 式启发检索，该表示在调用解析上更确定；相比把技能当作纯文本，它把分散在文档各处的约束与具体实现单元对齐。 实现支持 Python、JavaScript/TypeScript 与 Shell；在 515 个技能上得到 515 个 root、2,110 个 stage、2,261 个 context、3,351 个 plain、2,689 个 inline_code、575 个 ref_code 工作流节点与 7,077 个函数节点，工作流图规模中位数为 22 个节点。

意图掩码把节点上下文分成整体、谱系、邻居、自身四层，期望视图完全排除目标自身与实现内容，事实视图则逐步遮蔽声明上下文；多视图联合推理优于任何单一视图。 该机制直接回应“意图披露粒度”这一挑战：披露过多会让事实抽取偏向期望行为，披露过少会引入不合理的边界推断。 消融显示多视图确认 261 个缺陷、确认率 48.2%，而单视图为 228–236 个；所有单视图发现的并集只覆盖多视图发现的 97.7%，说明跨视图能发现任何单一视图都发现不了的缺陷；76.2% 的多视图发现被每个单视图共同确认。

候选缺陷在隔离 OpenCode 沙箱中验证：代码级用最小探针复现，工作流级构造可重放的触发场景，并记录 validated、refuted、skipped、failed 四种结论与轨迹日志。 把静态规格推理与动态验证结合，使缺陷假设必须落到可观察的运行证据上，而不是停留在文本比对。 跨全部后端共执行 6,933 个候选缺陷的验证，97.9% 得到确定结论；端到端成本 1,331 美元、平均每技能 2.585 美元，223 分钟完成，最多 30 个仓库并发。

该工作面向以 SKILL.md 声明意图为可信前提的技能仓库，适用于含显式工作流与可验证输出的技能，尤其是存在工作流—代码绑定的实现单元；作者指出对纯文本或创意类技能效果较弱，因为缺少确定性判定依据与端到端可执行性。方法当前覆盖 Python、JavaScript/TypeScript 与 Shell，可通过轻量适配器扩展其他语言。对使用者而言，它提供的是缺陷假设与可重放证据链，用于定位高风险单元，而非完整的形式正确性保证。

作者明确说明 SkillSpec 不提供完整形式正确性保证，规格是文本谓词而非可机器检验的证明；由于无法穷举真实仓库中的全部潜在缺陷，论文只报告精度而不报告召回率。残余假阳性呈现结构性差异：工作流假阳性中 68.5% 来自上游规格推理的过度推断，代码假阳性中 49.7% 涉及不可达触发；另有 19.8% 的工作流假阳性源于编排 LLM 在运行时以常识补偿了表面缺陷。节点级分析显示纯文本节点仍是主要瓶颈，工作流验证率跨后端在 29.3%–70.9% 之间，而代码候选始终高于 79.2%。此外，技能图分解本身不唯一，自然语言工作流允许多种合理抽象，评估采用冻结图基线以控制这一差异。若读者只读到摘要而缺少图表与附录，缺陷分类的完整判定细节与各数据集的分项数字仍需回到原文核对。