用途：Quint 用于为分布式协议等复杂系统编写可执行规格，可编译为 TLA+，并支持模拟与模型检验。
主要能力：提供模块与 import（Voting.*、Voting(quorum)、as 别名）；类型系统覆盖 int、bool、str、Set[T]、List[T]、映射 K -> V、元组、记录、联合类型与枚举；提供 Set/List/Map 运算符、记录不可变更新（{ ...n, phase: Propose }）、和类型构造与 match 模式匹配；支持 action 状态转移、all/any 合取析取、nondet 非确定性选择；支持不变量（@invariant）与时态属性（@temporal、eventually/always）；assume 声明常量前提（不会被 typecheck/run/verify 强制检查，需用 run 测试断言）。
使用方式：命令行提供 quint typecheck、quint run、quint test、quint verify；REPL 用 quint 或 quint -r spec.qnt::ModuleName，可用 :type 查看表达式类型。规格通常分为主模块 <protocol-name>.qnt（var、init、action、不变量、step 入口）与测试模块 <protocol-name>_test.qnt（import 主模块，含 run 测试与场景 witness）。quint run 的 --main 需传拥有被检查属性的模块。basicSpells 需显式导入：import basicSpells.* from "./basicSpells"，提供 Option、unwrap、require、values、transformValues、has、getOrElse、mapRemove、setRemove、find、max/min/abs 等。
适用场景：分布式协议建模、状态机规格与验证、需要模拟或模型检验的系统设计。
限制：语言存在硬性限制（如无字符串操作、无嵌套 match、无解构、无循环、无提前返回），详见 guidelines/constraints.md；assume 不被工具校验；Option 等并非内建，须依赖 basicSpells；本资料未提供收费、平台与价格信息。