用途：当已有 Quint 规范（.qnt 文件）并需要改动代码库时，用该技能把工作锚定在规范上。规范是系统必须做什么的形式化陈述，代码改动必须满足它。适用场景包括：重构（行为不变）、新增功能（与规范一致）、弥合代码与规范的漂移、以及规范先行变更。若尚无规范，需先用 quint-modeling 创建。
核心原则：规范即事实基准。研究、计划阶段由既有 .qnt 文件与紧凑的差距分析锚定，而非仅凭文字计划；只有通过第 3–4 阶段的验证门（实质性编辑后运行 Quint 工具）才继续实现。自然语言计划不是证明，工具结果才是。绝不要为了让验证通过而修改规范；如行为确实要变，先停下来向用户展示规范修改提案并获得批准。研究与计划阶段上下文利用率目标为 40–60%，紧凑编目代码库。
工作流：第 0 阶段定位，读规范明确其保证，澄清变更，判断是规范变更还是代码变更；小改动可跳过第 1 阶段。第 1 阶段研究，输出规范与代码间的紧凑差距分析（目标 300 行以内），逐状态变量与动作定位对应源码，找出无对应实现的缺口与规范未覆盖的代码行为。第 2 阶段计划，每步点名文件与函数、预期行为变化、用作验证门的 Quint 属性，并足够小以便独立验证；实施前先交用户评审，规范影响需明确批准。第 3 阶段实施，每步后运行 quint typecheck 并修复错误，再运行该步验证门（quint run / quint test / quint verify），失败则停下诊断并回到计划，不要把规范放松。每步后把状态压缩回计划文件。第 4 阶段验证，运行全部见证（预期违规，即目标状态可达）与全部安全不变量（预期无违规）；若有违反则回到第 2 阶段修计划；若见证被满足说明行为被过度约束，也需回到计划定位。
常用命令：quint typecheck；quint run（见证可达性、安全不变量，可用 --max-samples 5000）；quint verify；quint test；CLI 不足时可用 quint REPL 与 quint REPL eval。
禁止项：为通过失败不变量而改规范；跳过步间验证门；把整个代码库读入主上下文；仅以散文计划粗略实现；把规范当作参考文档；通过削弱不变量来修复失败。
限制：官方资料未提供具体安装方式、版本要求、收费与授权信息，也未给出实际运行示例输出，暂未提供。