Stats
Actions
Tags
From xspec
Use when the user asks for executable specifications, model checking, protocol verification, invariant proofs, state-machine modeling, race-condition debugging, or any task expressible as "verify property P holds in system S". Triggers (auto): - "spec this protocol", "model X formally", "executable spec for Y" - "verify invariant", "prove that Z", "is P always true?" - "can the system reach state W?", "reachability of ..." - "race condition in ...", "why does this concurrent code ..." - "state machine for ...", "transition system" - "counterexample", "explain this .itf.json", "trace failure" - "implement from this spec", "drive code from model" - "refactor the model", "update spec to match new requirements" Slash commands available: /xspec:setup, /xspec:status, /xspec:teardown, /xspec:spec:*, /xspec:verify:*, /xspec:code:*, /xspec:refactor:* Orchestrates the Quint CLI, quint-kb MCP, quint-lsp MCP, and 6 phase agents via a Dockerized runtime (no Claude Code inside container — pure tool surface).
How this skill is triggered — by the user, by Claude, or both
Slash command
/xspec:xspecThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
1. Check Docker daemon: `docker info > /dev/null 2>&1`. If fails → stop, tell
docker info > /dev/null 2>&1. If fails → stop, tell
user to start Docker.docker ps --filter name=^quint-runtime$ -q. If empty →
tell user to run /xspec:setup first. Stop.docker exec quint-runtime quint --version. If fails → suggest
/xspec:status then /xspec:setup. Stop.Once preflight passes, route to the appropriate command/agent for the user's question category.
| User intent | Route to |
|---|---|
| "I don't know where to start" | /xspec:spec:next |
| "Write a spec from these docs" | /xspec:spec:start |
| "Distributed protocol with message-passing" | /xspec:spec:setup-choreo then /xspec:spec:start |
| "Check my model is right" | /xspec:verify:start |
| "Can state X be reached?" | /xspec:verify:generate-witness |
| "Why does this counterexample happen?" | /xspec:verify:explain-trace |
| "Why can't scenario S be reached?" | /xspec:verify:debug-witness |
| "Are all message types reachable?" | /xspec:verify:check-types |
| "Are all listeners hit?" (Choreo) | /xspec:verify:check-listeners |
| "Implement from my spec" | /xspec:code:start then /xspec:code:orchestrate-migration |
| "Update spec for new requirements" | /xspec:refactor:start |
All Quint CLI calls MUST use docker exec quint-runtime quint .... See
@references/runtime-conventions.md for details.
The agents (analyzer, verifier, implementer, spec-implementer, mbt-validator, mbt-validator-standalone) load in isolated context. Dispatch them via the Task tool when:
verifier agent so main context stays clean)..artifacts/ (e.g. refactor
planning → analyzer).For one-shot questions ("what does this error mean?") stay in main context.
quint --help, quint typecheck output,
and reasoning over .itf.json files directly. Inform user that semantic
doc search is degraded; suggest restarting Claude Code session to pick up
MCP servers after /xspec:setup./xspec:setup to start./xspec:setup will build it (warn ~5-10 min).mcp__quint-kb__* or quint-lang.org/docs/./xspec:setup keeps user in control.npx claudepluginhub qdelettre/xspec --plugin xspecGuides creation, editing, and verification of skills for AI coding agents using test-driven development with subagent scenarios. Use when authoring or debugging skills.