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

markdown

## 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.

Context compaction pattern

After each step is verified, compact progress:

markdown

## Status (after Step N)
- Steps 1–N: DONE ✓
- Current: Step N+1
- Blocking issues: [none / description]
- Next verification gate: [invariant name]

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.

quint-execute-spec

NPX Install

Tags

SKILL.md Content