Counterexample-Guided Synthesis of Skill Applicability Contracts with Large Language Models

Agents reusing tool-calling skills need to know when they succeed and how they change the environment. We synthesize such applicability contracts from a supplied DSL and execution feedback, with the reference contract withheld. Our counterexample-guided inductive synthesis (CEGIS) loop partitions reachable states by the proposed contract's accept/reject predictions, executes the skill on both sides, and revises the contract from structured counterexamples. We evaluate synthesized contracts exhaustively over four core domains, three synthetic and one built on third-party tool code; a run counts as exact if its final contract is correct on every reachable state. Gemma-4-31B is exact in 20 of 20 seeds on Deployment and Calendar, against 0 and 3 for direct generation. On a finite $\tau$-bench retail fixture it is exact in 19 of 20, against 0 for direct generation and 3 for fixed-pool refinement. A common-loop factorial study of selection and termination retains the partitioning advantage for Gemma under both stopping rules after multiplicity correction; Qwen3.8 shows weaker, non-significant differences. Relational coverage has mixed effects across conditions. A Shopping difficulty study distinguishes recovery on a deliberately relaxed variant from failure when hidden rules become independently identifiable. Muse-Glimmer-30B is also exact in 20 of 20 seeds on Deployment and Calendar under its native low-reasoning setting. For local models, evidence chosen without the candidate fails mostly by false accepts; in local and hosted cohorts alike, the partitioned loop's residual failures are mostly false rejects hidden in the candidate's large predicted-reject region.