quint-execute-spec

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Execute the Quint Specification

执行Quint规范

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.

当你拥有Quint规范并希望对代码库进行变更时，本技能将工作锚定在规范之上。规范并非建议性文档——它是系统必须遵循的形式化声明。所有变更都必须满足规范要求。先评审规范，再进行代码开发。

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.

重构：在保留行为的前提下重组代码（规范保持不变；代码仍需满足规范）
新增功能：添加规范中描述或与规范一致的功能
差距对齐：代码已偏离规范，将其重新调整至符合规范
先规范后变更：先更新规范，再实现代码以满足更新后的规范

如果尚未存在规范，请先使用

quint-modeling

技能创建基础工件。

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.

本技能是闭环中的「后规范」环节：研究和规划以现有的

.qnt

文件和简洁的差距分析为锚点——而非仅依赖文字计划。实现仅在第3-4阶段的验证关卡通过后进行（实质性编辑后运行Quint工具）。自然语言计划并非证明；工具结果才是。

绝不能为了通过失败的验证而修改规范。 如果必须修改规范（有意变更行为），请停止操作，先向用户提交拟议的规范变更，再触碰任何代码。规范变更是影响力最高的评审节点。

上下文利用率目标：研究和规划阶段为40–60%。简洁地整理代码库信息，而非将所有内容读入主上下文。

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    │
└────────────────────────────────────────────────────────────┘

[Quint spec] + [Desired change description]
         ↓
┌────────────────────────────────────────────────────────────┐
│ 阶段0：定位方向                                             │
│   → 阅读规范：它能保证什么？                                 │
│   → 明确变更：需要哪些新行为？                               │
│   → 决策：这是规范变更还是代码变更？                         │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ 阶段1：研究（简洁版）                                       │
│   → 梳理规范与代码之间的差距                               │
│   → 输出：简洁的差距分析（目标：少于300行）                 │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ 阶段2：规划                                               │
│   → 精确步骤：要修改的文件、预期状态变化                     │
│   → 每个步骤：如何验证其满足规范要求                       │
│   → 确定每个关卡要运行的Quint属性                           │
│   → 实现前向用户提交计划                                   │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ 阶段3：实现                                               │
│   → 逐步遵循计划                                           │
│   → 每个阶段后：运行Quint工具，验证属性                     │
│   → 每个阶段后将简洁状态更新至计划中                       │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ 阶段4：验证                                               │
│   → 运行所有witnesses（预期结果为VIOLATED）                 │
│   → 运行所有invariants（预期无违规）                       │
│   → 若任何invariant失败：返回阶段2，修正计划                │
└────────────────────────────────────────────────────────────┘

Phase 0: Orient

阶段0：定位方向

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.

阅读规范并理解期望的变更。

阅读规范：它建模了什么？断言了哪些invariants？包含哪些witnesses？
阅读规范交接部分（若存在）：规范对应哪些源文件？
明确变更：询问用户：
- 哪些行为将变更？（对于重构：行为不应变更；对于新增功能：新增了什么？）
- 是需要修改规范，还是代码必须满足现有规范？
- 是否存在已失败的invariant，还是这是前瞻性变更？

轻量路径（简单变更可跳过研究）：如果变更很小（单个函数、一个模块、无新状态），跳过阶段1直接进入阶段2。

Phase 1: Research (Compact)

阶段1：研究（简洁版）

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.

对于非 trivial 的变更，生成规范与代码之间的简洁差距分析。保持聚焦——目标是简洁准确的摘要，而非完整读取代码库。回答以下问题：

给定位于
[规范路径]
的Quint规范和
[交接中的文件列表]
中的源文件：
对于规范中的每个状态变量，找到其在源代码中的管理位置

对于规范中的每个动作，找到源代码中对应的函数

识别规范中无对应源代码的行为（差距）

识别源代码中未被规范覆盖的行为（超出范围）
对于变更
[变更描述]
：哪些源文件会受影响？
输出简洁摘要。不要读取无关文件。目标：少于300行。

如果分析遗漏了关键内容，在继续前进行针对性的补充读取。

Phase 2: Plan

阶段2：规划

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

创建精确的实现计划。每个计划步骤必须：

指定要修改的文件和函数
描述预期状态变化（系统行为的变更内容）
指定作为验证关卡的Quint属性
足够小，可独立验证

Plan format

计划格式

markdown

undefined

markdown

undefined

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]

步骤1：[文件] — [变更内容]

Expected behavior change: [description]
Quint verification gate:
```
quint run
```
/
```
quint verify
```
— invariant
```
[name]
```

预期行为变更：[描述]
Quint验证关卡：
```
quint run
```
/
```
quint verify
```
— invariant
```
[名称]
```

Step 2: [file] — [what changes]

步骤2：[文件] — [变更内容]

...

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.

---

如果步骤N后invariant

[名称]

失败，停止操作并返回规划阶段。不得继续。


**实现前向用户提交计划。** 人工评审计划的影响力高于评审代码。

如果计划需要修改规范，需明确提交规范变更并先获得批准。

---

Phase 3: Implement

阶段3：实现

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.

遵循计划。每个步骤完成后：

运行
```
quint typecheck
```
并修复所有报告的错误。
运行步骤对应的验证关卡（
```
quint run
```
/
```
quint test
```
/
```
quint verify
```
）
如果关卡失败：停止操作，诊断问题，返回阶段2。不得通过放宽规范来修复问题。
每个步骤后将当前状态简洁地更新至计划文件中。这能让下一步的上下文窗口保持精简。

Context compaction pattern

上下文压缩模式

After each step is verified, compact progress:

markdown

undefined

每个步骤验证通过后，压缩进度：

markdown

undefined

Status (after Step N)

状态（步骤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.

步骤1–N：已完成 ✓
当前：步骤N+1
阻塞问题：[无 / 描述]
下一个验证关卡：[invariant名称]


将此内容写入计划文件。在复杂实现中，使用更新后的计划开启新的上下文窗口，而非在过载的上下文中继续。

Quint tool usage during implementation

实现过程中的Quint工具使用

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)

需求	工具
编辑后对规范进行类型检查	运行 `quint typecheck` ；继续前修复所有报告的错误
验证witnesses是否可达	使用witness作为invariant运行 `quint run`
验证安全invariants是否成立	运行 `quint run` 并添加 `--max-samples 5000` 参数，或运行 `quint verify`
交互式探索	`quint REPL session` + `quint REPL eval` （仅当CLI不足以满足需求时使用）

Phase 4: Verify

阶段4：验证

Run the full property suite.

运行完整的属性套件。

Witnesses (liveness check)

Witnesses（活性检查）

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

所有witnesses必须被违规（意味着预期状态可达）：

使用
```
quint run
```
并指定
```
witnesses
```
中的witness名称（或映射的invariant选择器）。
预期结果：报告witness可达性（等同于CLI原始输出中的
```
Counterexample found
```
）。

Safety invariants

安全Invariants

All invariants must not be violated:

Use
```
quint run
```
(or
```
quint verify
```
when stronger coverage needed).
Expected result: no invariant violation reported.

所有invariants必须未被违规：

使用
```
quint run
```
（或需要更强覆盖率时使用
```
quint verify
```
）。
预期结果：无invariant违规报告。

If a safety invariant is violated

如果安全Invariant被违规

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

逐步阅读反例追踪信息
识别引入违规的实现步骤
返回阶段2 — 修正计划，而非修改规范
如果规范中的invariant确实存在错误，向用户提交拟议的规范变更

If a witness is satisfied (action is unreachable)

如果Witness被满足（动作不可达）

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.

实现过度约束了行为——本应可达的路径被阻塞。返回阶段2并识别引入约束的步骤。

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.

如果期望的变更需要更新规范（新增状态变量、变更invariants）：

起草规范变更 — 在任何代码变更前向用户展示差异
独立验证更新后的规范 — 类型检查、运行witnesses、运行invariants
获得明确批准 — 规范变更获批前不得进行代码开发
然后实现代码以满足更新后的规范

这能在规范演进时仍保持其作为事实依据的地位。

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

反模式	为何会破坏工作流
修改规范以通过失败的验证	破坏了规范作为事实依据的地位
跳过步骤间的验证关卡	破坏了增量验证；bug会累积
将整个代码库读入主上下文	淹没上下文；应在阶段1中简洁整理
用文字计划，“大致”实现	计划必须足够精确，可逐步验证
将规范视为建议性文档	规范是形式化约束——可机器校验
通过弱化invariant来修复违规	必须在代码中修复invariant问题，而非放宽约束

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.

对于小而明确的变更（单个函数、无新状态）：

阅读相关的规范模块
识别覆盖变更行为的invariant(s)
进行变更
运行
```
quint run
```
并指定这些invariants
完成

跳过阶段0–1。仅对非trivial变更使用阶段2–4。