用途：Quint 是可执行规约语言，面向复杂系统（如分布式协议）。它编译为 TLA+，支持模拟与模型检查，用于形式化建模与验证。
主要能力：支持模块与导入（import Voting.*、import Voting(quorum)、import Voting as V）；类型系统含 int、bool、str、Set[T]、List[T]、K -> V 映射、元组、记录、和类型及枚举别名；定义分为 const（实例化时固定的模块参数）、pure def、def、val、pure val；状态变量仅在 val 定义与 action 中可读。action 描述状态转移并返回 bool，每个 var 必须在每个 action 中赋值，未改变用 x' = x；all { } 为合取，any { } 为析取，nondet 绑定支持非确定性选择。支持集合/列表/映射运算符、记录不可变更新（{ ...n, phase: Propose }）、和类型的 match 模式匹配、不变量与时间属性（eventually、always）、assume 前提、if 与 let。
使用方式：通过 CLI 校验与执行——quint typecheck、quint run、quint test、quint verify；仅在需要表达式级交互时打开 REPL（quint 或 quint -r spec.qnt::ModuleName）。规约通常分两文件：主模块声明状态变量、init、actions、不变量，step 必须位于主模块；测试模块通过 import myProtocol.* 引入主模块，包含 run 测试与场景见证。quint run 的 --main 应为拥有被检查属性的模块。basicSpells 标准库通过 import basicSpells.* from "./basicSpells" 引入，提供 Option（Quint 无内置 Option）、unwrap、require、values、transformValues、has、getOrElse、mapRemove、setRemove、find、max/min/abs 等；罕见运算符见 rareSpells.qnt。
限制：assume 不被强制检查，违背后被 typecheck、run、verify 静默忽略，需用 quint test 的 run 测试断言常量条件。语言存在硬性限制：无字符串操作、无嵌套 match、无解构、无循环、无提前返回（详见 guidelines/constraints.md）。其他收费、价格、平台与效果信息暂未提供。