Implement code against an existing Quint specification. Uses Research → Plan → Implement workflow (ACE-FCA style) grounded by the spec as the source of truth. Use when the user wants to refactor code, add a new feature, or close a gap between implementation and spec — with the Quint spec as the formal constraint that all changes must satisfy.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
Implement code against an existing Quint specification. Uses Research → Plan → Implement workflow (ACE-FCA style) grounded by the spec as the source of truth. Use when the user wants to refactor code, add a new feature, or close a gap between implementation and spec — with the Quint spec as the formal constraint that all changes must satisfy.
Execute the Quint Specification
When you have a Quint spec and want to make a change to the codebase, this skill grounds the work
in the spec. The spec is not advisory — it is the formal statement of what the system must do.
All changes must satisfy it. The spec is reviewed, then the code follows.
When to use this skill
Refactor: restructure code while preserving behavior (spec stays fixed; code must still satisfy it)
New feature: add functionality described by or consistent with the spec
Gap closure: code has drifted from the spec; bring it back into alignment
Spec-first change: update the spec first, then implement to satisfy it
If no spec exists yet, use quint-modeling first to create the grounding artifact.
Core principle: spec is ground truth
This skill is the post-spec half of the loop: Research and Plan are anchored by the
existing .qnt file and compact gap analysis—not by prose plans alone. Implement proceeds only
with the verification gates in Phases 3–4 (Quint tool runs after substantive edits). Natural-language
plans are not proof; tool results are.
Never modify the spec to make a failing verification pass.
If the spec must change (behavior is intentionally changing), stop and present the proposed spec
change to the user before touching any code. The spec change is the highest-leverage review point.
Context utilization target: 40–60% during research and planning. Catalog the codebase compactly
rather than reading everything into the main context.
Workflow
[Quint spec] + [Desired change description]
↓
┌────────────────────────────────────────────────────────────┐
│ Phase 0: Orient │
│ → Read the spec: what does it guarantee? │
│ → Clarify the change: what new behavior is needed? │
│ → Decide: is this a spec change or a code change? │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Phase 1: Research (compact) │
│ → Map the gap between spec and code │
│ → Output: compact gap analysis (target: under 300 lines) │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Phase 2: Plan │
│ → Precise steps: files to change, expected state delta │
│ → For each step: how to verify it satisfies the spec │
│ → Identify which Quint properties to run at each gate │
│ → Present plan to user before implementing │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Phase 3: Implement │
│ → Follow plan phase by phase │
│ → After each phase: run Quint tools, verify properties │
│ → Compact status back into the plan after each phase │
└────────────────────────────────────────────────────────────┘
↓
┌────────────────────────────────────────────────────────────┐
│ Phase 4: Verify │
│ → Run all witnesses (expect VIOLATED) │
│ → Run all invariants (expect no violation) │
│ → If any invariant fails: return to Phase 2, fix plan │
└────────────────────────────────────────────────────────────┘
Phase 0: Orient
Read the spec and understand the desired change.
Read the spec. What does it model? What invariants does it assert? What witnesses does it have?
Read the Spec Handoff section (if present). Which source files does the spec correspond to?
Clarify the change. Ask the user:
What behavior is changing? (for refactors: nothing should change; for features: what is new?)
Should the spec change, or must the code satisfy the existing spec?
Is there an existing failing invariant, or is this forward-looking?
Lightweight path (skip research for simple changes):
If the change is small (single function, one module, no new state), skip Phase 1 and go straight
to Phase 2.
Phase 1: Research (Compact)
For non-trivial changes, produce a compact gap analysis between spec and code. Keep this focused —
the goal is a compact, accurate summary, not a full codebase read. Answer these questions:
Given the Quint spec at [spec path] and the source files [file list from handoff]:
For each state variable in the spec, find where it is managed in source code
For each action in the spec, find the corresponding function(s) in source code
Identify any spec behaviors that have no corresponding source code (gaps)
Identify any source code behaviors not captured in the spec (out-of-scope)
For the change [change description]: which source files are affected?
Output a compact summary. Do not read files that are not relevant. Target: under 300 lines.
If the analysis missed something critical, do a targeted follow-up read before proceeding.
Phase 2: Plan
Create a precise implementation plan. Each plan step must:
Name the file and function to change
Describe the expected state delta (what changes in the system's behavior)
Specify the Quint property to run as a verification gate
Be small enough to verify independently
Plan format
## Change: [one-sentence description]### Spec impact- Properties that must continue to hold: [list]
- Properties that will change (if any): [list] — REQUIRES USER APPROVAL BEFORE IMPLEMENTATION
### Implementation steps#### Step 1: [file] — [what changes]- Expected behavior change: [description]
- Quint verification gate: `quint run` / `quint verify` — invariant `[name]`#### Step 2: [file] — [what changes]
...
### Rollback criteria
If invariant `[name]` fails after Step N, stop and return to planning. Do not proceed.
Present the plan to the user before implementing. Human review of the plan has higher leverage
than review of the code.
If the plan requires modifying the spec, present the spec change explicitly and get approval first.
Phase 3: Implement
Follow the plan. After each step:
Run quint typecheck and fix all reported errors.
Run the step's verification gate (quint run / quint test / quint verify)
If the gate fails: stop, diagnose, return to Phase 2. Do NOT fix by loosening the spec.
Compact current status back into the plan file after each step. This keeps the context window
lean for the next step.
Write this to the plan file. In complex implementations, start a new context window with the
updated plan rather than continuing in an overloaded context.
Quint tool usage during implementation
Need
Tool
Type-check spec after any edit
Run quint typecheck; fix all reported errors before continuing
Verify witnesses are reachable
quint run with witness as invariant
Verify safety invariants hold
quint run with --max-samples 5000 or quint verify
Interactive exploration
quint REPL session + quint REPL eval (only when CLI is insufficient)
Phase 4: Verify
Run the full property suite.
Witnesses (liveness check)
All witnesses must be violated (meaning the expected state is reachable):
Use quint run with witness name in witnesses (or mapped invariant selector).
Expected result: witness reachability is reported (equivalent to Counterexample found in raw CLI wording).
Safety invariants
All invariants must not be violated:
Use quint run (or quint verify when stronger coverage needed).
Expected result: no invariant violation reported.
If a safety invariant is violated
Read the counterexample trace step by step
Identify which implementation step introduced the violation
Return to Phase 2 — fix the plan, not the spec
If the spec's invariant is genuinely wrong, present the proposed spec change to the user
If a witness is satisfied (action is unreachable)
The implementation has over-constrained behavior — a path that should be reachable is blocked.
Return to Phase 2 and identify which step introduced the constraint.
Spec change protocol
If the desired change requires updating the spec (new state variables, changed invariants):
Draft the spec change — show the diff to the user before any code changes
Verify the updated spec in isolation — typecheck, run witnesses, run invariants
Get explicit approval — do not proceed to code until the spec change is approved
Then implement the code to satisfy the updated spec
This preserves the spec as the source of truth even when it evolves.
What NOT to do
Anti-pattern
Why it breaks the workflow
Modify spec to pass a failing invariant
Destroys the spec as ground truth
Skip verification gates between steps
Breaks incremental verification; bugs compound
Read the whole codebase into main context
Floods context; catalog compactly in Phase 1 instead
Plan in prose, implement "roughly"
Plan must be precise enough to verify step-by-step
Treat spec as advisory documentation
Spec is a formal constraint — machine-checkable
Fix invariant failure by weakening the invariant
Invariants must be fixed in code, not loosened
Lightweight path for simple changes
For small, well-understood changes (single function, no new state):
Read the relevant spec module
Identify which invariant(s) cover the changed behavior
Make the change
Run quint run with those invariants
Done
Skip Phase 0–1. Use Phases 2–4 only for non-trivial changes.
