用途：把用户给出的系统、协议或算法转成 Quint 规范，覆盖建模、规格化、形式化描述与模型检查准备。技能本身负责建模方法，语言语法、算子、CLI 与 basicSpells 交给 quint-lang 参考。
入口流程按起点选择：仅有一个想法用 from-nothing；已有需求或功能规格文档用 from-requirements；已有 Rust、Go、TypeScript 等源码用 from-code；已有 TLA+ 规范用 from-tlaplus；已有 .qnt 规范要审计用 review（不产出新模型，按清单审查并报告）。起点不明确时应先问用户哪种来源为准。
共享建模主线：先区分关注点，把状态机（var、init、actions）、纯函数逻辑（pure def）与性质（val 不变量、witness、时序性质）分开，并用 const 固化为系统模型假设（通信、故障、时间、参与者）；再塑造状态，按参与者数量决定单个 record 还是 Id -> LocalState 映射，按通信方式决定消息 soup、共享内存或按对有序队列；分布式消息传递协议默认用 Choreo 框架，除非单参与者或共享内存协调，或小协议中脚手架明显更冗长。随后写纯函数：guard 判断能否发生，apply 计算新状态；先写签名并 typecheck，再逐个在 REPL 中用手工状态验证。
必要用法与限制：规范应从一开始就可执行，每一步后用 quint typecheck 再 quint run 验证；只运行 quint run，不要使用 quint verify，除非用户明确要求模型检查。注意未赋值的 const 可以通过 typecheck 但 quint run 会报 Uninitialized const，需在具体实例模块中实例化后运行，例如 module spec_3 { import spec(C = Set(1,2,3)).* }。assume 只记录前提，不提供取值。建模遵循“描述什么而非如何实现”，抽象掉序列化、内存管理等与不变量无关的细节。examples/ 中提供了消息传递的 tendermint 与共享状态的 ewd426.qnt 两个完整可运行参考。其他细节暂未提供。