SkillSpec turns skill correctness into intent-masked specification reasoning: 763 confirmed defects across 515 real-world skills, 67.1% precision on code nodes

The paper reframes agent skill correctness as a consistency problem between declared intent and encoded behavior, adapting Hoare triples by decomposing a skill into operational units with textual precondition and postcondition predicates. Prior work on skills focused on benchmarks, capability enhancement, and security attacks, leaving non-malicious defects largely unexplored; this work extends classical Hoare reasoning from code to artifacts that interleave natural-language instructions with heterogeneous resources. The paper gives a formal definition (ExpectSpec from complete declared intent, FactSpec from implementation under masked intent) and illustrates it with an audio-concatenation operation where an undeclared side effect surfaces; the authors state these are textual predicates, not a machine-checkable proof system.

SkillSpec builds a unified representation: SKILL.md is reconstructed as a typed workflow DAG with contain and dependency edges, scripts are parsed via Tree-sitter into a language-agnostic IR with a call graph, and intent-implementation binding creates a bidirectional mapping between workflow units and code nodes. Compared with the grep-based heuristics common among LLM agents, this representation resolves calls deterministically; compared with treating skills as plain text, it aligns constraints scattered across the document with concrete implementation units. The implementation supports Python, JavaScript/TypeScript, and Shell; across 515 skills it yields 515 root, 2,110 stage, 2,261 context, 3,351 plain, 2,689 inline_code, and 575 ref_code workflow nodes plus 7,077 function nodes, with a median of 22 workflow nodes per SKILL.md.

An intent mask organizes node context into holistic, lineage, neighbor, and self layers; the expectation view excludes the target itself and all implementation content, while factual views progressively mask declarative context, and joint multi-view reasoning outperforms any single view. This mechanism directly addresses the intent-disclosure-granularity challenge: too much disclosure biases factual extraction toward expected behavior, too little admits implausible boundary inferences. The ablation shows multi-view confirms 261 defects at a 48.2% confirmation rate versus 228-236 for individual views; the union of all single-view findings covers only 97.7% of multi-view findings, and 76.2% of multi-view findings are confirmed by every single view.

Candidate defects are validated in an isolated OpenCode sandbox: code-level candidates are reproduced with minimal probes, workflow-level candidates are corroborated by replayable trigger scenarios, and each run records validated, refuted, skipped, or failed verdicts with trajectories and logs. Combining static specification reasoning with dynamic validation forces defect hypotheses to rest on observable runtime evidence rather than textual comparison alone. Across all backends, 6,933 candidate defects were executed in validation and 97.9% received conclusive verdicts; end-to-end cost was $1,331, averaging $2.585 per skill, completing in 223 minutes with up to 30 repositories processed concurrently.

The work targets skill repositories whose SKILL.md declared intent is assumed to faithfully reflect true intent, and applies to skills with explicit workflows and verifiable outputs, especially implementation units with workflow-code bindings; the authors note weaker effectiveness on plain-text or creative skills where deterministic oracles and end-to-end executability are unavailable. The method currently covers Python, JavaScript/TypeScript, and Shell, extensible to other languages through lightweight adapters. For practitioners it supplies defect hypotheses with replayable evidence chains for localizing high-risk units, not a complete formal correctness guarantee.

The authors state SkillSpec does not provide complete formal correctness guarantees and that specifications are textual predicates rather than machine-checkable proofs; because exhaustively enumerating latent defects in real repositories is intractable, the paper reports precision but not recall. Residual false positives show structural patterns: 68.5% of workflow false positives come from over-inference in upstream specification reasoning, 49.7% of code false positives involve unreachable triggers, and 19.8% of workflow false positives reflect external compensation where the orchestrating LLM repairs an apparent defect at runtime. Node-level analysis shows plain-text nodes remain the main bottleneck, with workflow validation rates spanning 29.3%-70.9% across backends while code candidates consistently exceed 79.2%. Skill graph decomposition is also inherently non-unique, since natural-language workflows admit multiple plausible abstractions, and the evaluation freezes a graph baseline to control this. A reader who sees only the abstract without figures and appendices would still need the full text to check the complete defect-category judgments and per-dataset breakdowns.