用途：把用户给出的系统、协议或算法转写为 Quint 形式化规格，支持建模、规格化描述、模型检查与验证类需求。
主要能力：按起点选择流程——仅有想法（从零交互式构建）、需求/功能规格文档、源代码（Rust、Go、TypeScript 等）、既有 TLA+ 规格；另有一条 review 流程，用于按清单审查已完成的 .qnt 规格并报告发现，而非新建模型。语法、运算符、CLI 与 basicSpells 参考 quint-lang。
使用方式：内部分为三步主干。先分离关注点——状态机（var、init、actions）、功能逻辑（纯 def）、性质（不变式与见证，活性用时序性质），并把系统模型假设（通信方式、故障模型、时间模型、参与者与本地状态）写成 const。再塑造状态——按参与者数量决定单一 record 还是 Id -> LocalState 映射；按通信方式决定消息通道（无序 Set[Message] 为默认、有序逐对队列仅在顺序关键时使用、共享内存则无消息变量）；分布式消息传递协议默认用 Choreo 框架，需要说明理由才改用普通 Quint。最后以纯函数写功能逻辑：把“能否发生”写成 bool 守卫，把“结果状态”写成返回 State 的纯 def，先写签名并 typecheck，再逐个在 REPL 中用手工构造的状态验证。
限制与注意：规格要“从第一行即可执行”，每加一步都要 quint typecheck 后 quint run；仅 typecheck 不够，未赋值的 const 能通过类型检查但运行报 Uninitialized const，需在具体实例模块中实例化该 const（如 module spec_3 { import spec(C = Set(1,2,3)).* }）。全程只用 quint run，不用 quint verify；verify 是穷尽的有界模型检查（Apalache），耗时更长，仅在用户明确要求模型检查时使用。assume 只记录前提而不提供取值，也不作为检查手段，需用运行测试断言假设。建模关注可观察的状态转移，抽象掉序列化、内存管理、重试等实现细节。示例参考：examples/tendermint/（消息传递，真实 BFT 共识）、examples/ewd426.qnt（共享状态，令牌环）。本资料未提供安装方式与收费信息。