外观
VIGIL：将 Agent Skill 行为规范编译为运行时约束
摘要
Skill 文档可以声明权限、披露限制和前置条件，但自然语言本身不会阻止 Agent 在多次工具调用后违反这些要求。VIGIL 把 Skill 规范转换为有限轨迹上的 SMT 约束，检查事件顺序、参数关系和跨调用值流，并在发现违规时干预。
作者在 152 条真实 Agent 轨迹（72 条违规、80 条良性）上比较 VIGIL 与运行时基线，覆盖办公文档、运维和 Skill 注入场景。该结果支持“执行轨迹需要可计算规范”的研究方向，但不等于所有 Skill 或任意 Agent 已获得安全保证。
核心创新与差异
本站已有 Skill 安装扫描、权限声明和动态差分；VIGIL 的差异是把规范的时序、参数和值流语义推进到执行面，而不是只在安装或单次调用时检查。
威胁模型与攻击链
攻击者可提供含恶意边界的 Skill、诱导 Agent 组合多个看似合法的调用，或利用跨调用数据流泄露秘密。首个失效控制是文档规范没有对应的确定性运行时执行点，修复责任在 Agent runtime 与 Skill 维护者。
实验设计与实际过程
作者从 SkillsBench 与 Skill-Inject 构造标注轨迹，使用 AgentDojo、SafeAgentBench 做交叉比较，并报告检测效果、消融和运行开销。VIGIL 的 SMT 规则在有限轨迹上执行；这是作者实验，本站未复现。
关键结果与实际影响
评测分母为 152 条轨迹，包含 72 条违规与 80 条良性样本。论文显示跨事件约束可以捕获固定调用过滤器看不到的违规；具体指标、运行时间和基线应以原论文表格为准。有限轨迹标签和框架选择限制了外推。
防护措施与验证方法
把 Skill 声明拆成可验证的时序、参数和值流规则；在副作用调用前使用默认拒绝的执行器，并记录规则版本、轨迹和拒绝原因。验证应包含跨调用组合、更新后重验、良性误报和轨迹长度开销。
局限与待验证问题
评测依赖有限事件模型、自动或半自动标签和受控 Skill 集，尚无独立复现与生产负载测试。需要验证未见过的工具、长会话和规则冲突。