为 Quint 规范设计的确定性 linter。quint-audit 读取现有的 .qnt 文件，将 quint 自身的 parse IR 解码为类型化的 OCaml 结构，并报告结构性问题。不涉及 LLM，也不调用 quint verify。

状态：v0.1.0。check id、退出码和报告 schema 是稳定的契约。各项检查的语义在 Quint 中建模，并通过变异体测试验证（变异体全部被杀死）。每项检查都针对一个包含 67 个规范的真实语料库进行了对抗性审查。在 v0.x 期间仍然暂定的是：各项检查的严重级别和消息措辞，随着语料库的增长可能会调整。

Quint Studio 会对它生成的规范运行质量检查，但到目前为止还无法处理手写的规范。Quint 团队已经说明，目前没有从现有 .qnt 文件转换为 Studio 组件形态的路径。

quint-audit 将 Quint LLM kit 的 review checklist 应用于任何现有的 .qnt 规范，并增加了 checklist 未覆盖的生产环境陷阱检查。检查的名称和报告的条目沿用该 checklist，因此输出对 Quint 社区来说应该读起来很熟悉。检查结果带有 span、严重级别、修复建议和退出码，同时提供人类可读的报告和稳定的 JSON 文档。quint-audit 是为 CI 而构建的。

quint verify 回答的是“不变量是否在 N 步内被打破？”。它无法回答规范是否构建良好。一个 action 跳过了某个变量、一个恒真的不变量、一个死分支、一个缺失的见证：这些都不是模型检查能回答的问题。一个规范可以验证通过，但仍然是空洞的或难以维护的。quint-audit 以解析的成本提出构建纪律方面的问题。

Quint LLM kit 的 review 是模型对单个规范的判断；quint-audit 是确定性检查器，对相同的输入和参数，IR 运行产生逐字节相同的结果。其检查语义在 Quint 中建模，在本仓库中验证，并通过变异体测试来检验。LLM kit 的 checklist 是模型解读的散文。quint-audit 沿导入图追踪，将检查结果归属到各自所属的文件并去重；它以解析成本在 CI 中运行，带有退出码、JSON schema、稳定的 check id，且不引入模型。LLM kit 的 review 在交互场景下更深入：它驱动 REPL，展示违规时的状态，包含逐 action 见证检查和对话式修复循环；quint-audit 是它旁边的批量检测工具，而非替代品。

quint-audit 读取规范的字节内容。非 ASCII 源文件会被拒绝，并给出第一个违规字节的偏移量。source map 的索引是 UTF-16 code unit；非 ASCII 字符会使其后所有 span 发生偏移，导致 span 无法指向它所报告的字节。

它在 60 秒超时下运行 quint parse --out <ir.json> --source-map <map.json>。解析失败是退出码 2，绝不会是 lint 报告。

类型化解码器会校验每个被消费的 IR 字段。格式错误的 IR 会导致解码失败，并指明 JSON 字段路径。解码器从不为被消费的字段替换默认值。未知的 IR 节点类型会被保留：需要该节点的检查会报告 info 级别的覆盖缺口，绝不会报告为通过。

IR 检查按模块运行。名称解析是模块局部的。

完整运行时，驱动运行的检查在三种状态纪律下采样 trace：passed 要求退出码为 0 且运行自身的成功摘要；failed 要求失败摘要；其他一切均为 did-not-run，退出码 2。超时不算通过。

报告会打印出来，进程以 0、1 或 2 退出。

安装 从源码安装。需要 OCaml 5.3、dune 和 opam。

opam install . --yes

或者不安装直接构建：

opam exec -- dune build

binary: _build/default/bin/quint_audit_cli.exe

Quint 本身是运行时依赖。安装 quint 0.33.1：

npm i @informalsystems/quint@0.33.1 -g

quint-audit 会在 PATH 中查找 quint，也可以通过 --quint /path/to/quint 指定显式路径。

支持的 quint 版本：0.33.1。锁定这个版本是因为类型化解码器是针对该版本的 parse-IR 形态编写的。工具会在报告中记录 quint 的版本字符串，但从不比较它。较新的 quint 只要保留被消费的字段就仍然可用。如果移动了某个字段，则会明确失败：解码错误会指明 JSON 路径，进程以 2 退出。开发语料库（见“验证”部分）是更广泛的漂移检测器：每次检查变更在合入前都会在 67 个真实规范上全面运行。

quint-audit lint path/to/spec.qnt quint-audit lint --format=json path/to/spec.qnt quint-audit lint --fail-on=warn path/to/spec.qnt quint-audit lint --quint /path/to/quint path/to/spec.qnt quint-audit full path/to/spec.qnt quint-audit full --max-samples 10 --max-steps 20 --seed 0x2
--invariant=i_safety path/to/spec.qnt

lint 运行确定性的 IR 检查：QL001、QL002、QL003、QL006、QL008、QL009、QP001、QP002。

full 增加驱动运行的检查：QL004 见证、QL007 init 执行、QL010 init 处的不变量、QL011 action 之后的不变量。

每次 quint 运行都是固定参数的：后端、详细程度、显式的样本数量和显式的步数上限。这些固定参数会随报告一起打印。带种子的运行仍然显式传入样本数量，因为一旦提供种子，quint 会将其默认值降为 1。

--invariant NAME（可重复）指定要作为不变量求值的 val 声明。未提供名称时，不进行任何求值：QL010 和 QL011 报告为 not-evaluated，并且默认绝不会通过。

--run-timeout SECONDS 限制单次 quint 运行的时长（默认 120）。

退出码

code meaning 0 没有达到或超过门限阈值的检查结果 1 至少有一个达到或超过阈值的检查结果。默认阈值是 fail；--fail-on=warn 会降低阈值，也会因 warning 而失败 2 审计无法运行：用法错误、缺少 quint、非 ASCII 输入、解析失败、类型化解码失败、运行未执行或内部错误

退出码 2 绝不表示规范违规。门禁可以区分“规范违反了规则”和“linter 无法运行”。

--format=json 输出稳定的文档。schema 随附于 docs/report-schema.json。字段名是固定的。findings 是扁平、去重后的列表；sources 包含

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）