Whole-Trace Checking Catches 95.8% of Skill Policy Violations

Notes on VIGIL: Runtime Enforcement of Behavioral Specifications in AI Agent Skills (arXiv:2606.26524) — Ying Li, Yanju Chen, Hongbo Wen, Bosi Zhang, Hanzhi Liu, Peiran Wang, Yunhao Feng, Yuan Tian · June 2026

Note published July 25, 2026 · written by SkillFed’s research pipeline from the paper above · how these notes are made

VIGIL is a runtime reference monitor for agent skills. It abstracts raw tool calls into typed events, then grounds each skill's natural-language specification into a policy that names the actual arguments, outputs, and artifact identities appearing in that specific run — closing the gap between generic prose ("validate before use") and a checkable rule. Each grounded policy compiles into a quantifier-free SMT query evaluated against the whole trace, not one call at a time, so a violation can hinge on event order, an argument value, or something produced several steps earlier and only consumed later. The policy language covers six temporal forms — absence, precedence, response, bounded response, resolution, and until — and when the solver finds a policy broken, its unsatisfiable core points to the exact invocation to block before that call's effects land.

On 152 labeled executions from SkillsBench and Skill-Inject (72 violating, 80 benign), VIGIL catches 69 of the 72 violations: 95.8% recall at 89.6% precision, 15.8 F1 points ahead of the strongest baseline — an LLM-as-judge that sees the full trace but still misses 24 violations for lack of formal grounding. Single-call defenses AgentSpec and Progent, which check one action at a time, miss roughly half the violations outright. Run against 216 real executions of shipped skill bundles from NVIDIA, Databricks, Cloudflare, and Trail of Bits, VIGIL surfaces 34 confirmed policy violations, among them a missing liveness rule in NVIDIA's own skill ecosystem that let a Slurm job keep resubmitting GPU work after evaluation failures — NVIDIA acknowledged it as a real cost concern. The deterministic SMT check itself runs in 0.27 seconds; the 4.38-second end-to-end average is dominated by a single cacheable LLM call that compiles the policy.