theagenticguy/symspec

# symspec [](LICENSE) **symspec 让你编写出的软件需求规格说明书不仅*可以证明*是一致的，而且在无法证明时也会坦诚相告。** 你只需用通俗易懂、结构化的自然语句描述系统应有的行为；symspec 会将每一句转化为清晰的需求， 而一个数学证明器（Z3，可选择使用 Lean 4 进行复核）要么**证明**其中的某两项不可能同时成立——并指出确切的冲突来源——要么返回 `verified: false` 并为你提供一份精确的任务清单，告诉你如何让这份规格说明书具备可证明性。 最后一部分才是核心所在。大多数所谓的“规格审查”只不过是让大语言模型写一段看似自信的段落，却漏掉了真正的矛盾。symspec 将这种检查变成了**机械化的过程**：矛盾要么被证明存在，要么不存在；而*“已验证 (verified)”*这一声明，除非证明器真正将其推导出来，否则该工具绝不轻易做出。模糊的相似度评分永远无法为你的规格背书，只有可靠的证明才能做到。 它既适用于编写规格说明书的人类，也适用于由编码 agent 驱动的场景：每一条命令都会以结构化的 JSON 和稳定的退出代码作为响应，让 agent 始终清楚自己是否执行成功以及下一步该做什么——而人类则可以通过 `--pretty` 阅读相同的结果。 *（初次接触？文中所有缩写都会在首次出现时给出全称，在文末还有一个通俗易懂的[词汇表](#glossary)。建议从[什么是需求，以及“证明”它的含义](#what-a-requirement-is-and-what-proving-it-means)开始阅读。）* ## 快速开始 ``` # 全局安装命令行工具 git clone https://github.com/theagenticguy/symspec.git && cd symspec pnpm install && pnpm build && pnpm pack npm install -g ./symspec-*.tgz # puts the `symspec` command on your PATH # 一次性：获取 always-on meaning-similarity tier 运行所需的本地 embedding model（约 110 MB，sha256-pinned）。 # 此后完全离线。 symspec download-model ``` symspec 采用 **EARS** 风格（Easy Approach to Requirements Syntax，需求语法简易方法——一种小型的句子模板集合，例如*“当发生 X 时，系统应当执行 Y”*）。你只需提供各个要素；它就会生成句子，并确保整个集合保持一致。 创建一个文档，添加两项需求，然后对它们进行检查。每条命令默认都会以结构化数据 (JSON) 的形式输出结果： ``` $ symspec init reqs.symspec.json $ symspec add reqs.symspec.json --pattern event-driven --system "auth service" \ --response "grant access" --trigger "the user submits valid credentials" $ symspec add reqs.symspec.json --pattern event-driven --system "auth service" \ --response "revoke access" --trigger "the user submits valid credentials" $ symspec check reqs.symspec.json ``` 这两项需求相互矛盾——其中一个在某个事件发生时授予访问权限，而另一个则在完全相同的事件下撤销了权限——`check` 命令会捕捉到这一点，指出存在问题的两项需求，并展示其推导过程： ``` { "apiVersion": 1, "type": "check", "data": { "findings": [ { "code": "FND_CONTRADICTION", "severity": "error", "requirementIds": ["586d8933-…", "d50c8fff-…"], "message": "Requirements 586d8933…, d50c8fff… cannot all hold: on the same trigger, one grants access and the other revokes it.", "evidence": { "...": "the exact reasoning the checker used" } } ], "counts": { "error": 1, "warn": 0, "info": 0 } } } # 该命令也会以状态码 1 退出 — 发现了 blocking problem。 ``` **退出状态码就是通过或失败的信号**，因此脚本或 CI 流水线可以直接将其作为门禁，而无需读取输出内容：`0` = 无误（或仅有警告），`1` = 发现了阻塞性问题，`2` = 命令本身无法运行（参数错误、文件缺失、模型缺失），`3` = `--strict` 严格门禁判定本次运行*结论不明 (inconclusive)*——虽然没有被证明存在错误，但该规格说明书同样无法被验证为正确，而输出结果会确切地告诉你原因。 **让你的 agent 自行完成设置。** 运行 `symspec install`，它会在你正在使用的任意一款 AI 编程助手（无论是 Claude Code、Cursor、Codex、Kiro、Windsurf 还是 GitHub Copilot）中放入一个小型的“技能”文件，让助手学会自主使用 symspec。它只会写入到各个工具专属的 skills 文件夹中，绝不会修改你现有的指令文件。 ## 什么是需求，以及“证明”它的含义 **需求 (Requirement)** 是对系统必须执行的操作的一项陈述——*“当用户登录时，系统应当发放一个 token。”*而**规格说明书 (Spec)** 则是这一系列需求的集合。需求正是软件在任何人编写代码*之前*就出问题的地方：两项需求暗中相互矛盾、一句话偷偷捆绑了两个不同的要求，或者同一个速度限制在这里被写成“2秒以内”，而在那里却被写成“3秒以上”。人类往往会一眼略过这些问题，而被要求“以文字形式审查规格说明书”的大语言模型也是如此。 symspec 绝不会仅停留在文字层面的审查。它会进行**证明 (prove)**。在底层，它会将你的需求转化为逻辑表达式，并交给一个 SMT 求解器——**Z3**（一款成熟的自动化定理证明器）——它会确切地回答这一个问题：*是否存在一种方式可以让所有这些条件同时成立？*如果答案是不存在，那这就不仅是一种观点——而是一个数学事实。随后，symspec 会报告 **unsat core（无法满足的核心）**：即已经存在冲突的最小需求子集，从而让你能够对症下药，而不是盲目猜测。 有两项保证界定了这种证明的适用范围，symspec 对此均做出了明确的声明，避免让你产生过度联想： - **当 symspec 证明了某个冲突时，该冲突必然是真实的。**绝无虚惊一场——捏造出来的矛盾是该工具从设计上绝对不允许出现的唯一一种错误。 - **沉默并不等于认证合格。**由于两项措辞不同的需求可能描述的是同一件事，symspec 可能会*遗漏*隐藏在不匹配词汇背后的冲突。一个“无误”的结果仅仅意味着*“没有发现被证明为错误的问题”*，而绝不意味着*“绝对完美无缺”*。这也是为什么 `verified: true` 是需要努力争取才能获得的，而不是理所当然的假设——详见[诚实的判定结果](#honest-verdicts--verified-false-and-the-work-list)。 这一诚实的局限性，恰好是下一节所要填补的。 ## 将含义编码进规格说明书——神经符号核心 这就是纯粹的逻辑检查器无法单独解决的问题。以一个输液泵为例，假设有以下两项需求： 对你来说，它们显然相互冲突——30分钟不可能同时也是60分钟。但对于一个只会字面比对的检查器来说，它们是两个截然不同的量：一个与*完成*有关，另一个与*运行*有关。因为字面上不匹配，所以一个简单的工具什么也不会比较，直接报告一切正常。这正是真正的冲突得以隐藏的漏洞所在。 symspec 通过两个**绝不会混淆**的动作填补了这一空白——这种分离正是其设计的核心： 1. **提议（模糊部分）。** 一个在你**本地机器上**运行的小型语言模型会衡量两种措辞在含义上的接近程度，同时确定性的检测器会捕捉结构上的特征——针对同一对象、方向相反、数值边界对立。在上述输液泵的例子中，symspec 注意到这两项需求在同一触发条件下对同一事物设定了截然相反的数值边界，于是发出了一条 *info（信息）*级别的发现：`FND_QUANTITY_ALIAS_CANDIDATE`，其中携带了**确切的命令**，用以告诉系统这两种措辞指的是同一个量：`symspec glossary add "complete the infusion" "run the infusion"`。在你执行该命令之前，symspec **绝不会**声称该规格说明书是一致的——它会将状态标记为 `verified: false`，因为它知道自己实际上还未对这两者进行过比较。 2. **决定（可靠部分）。** 一旦你提交了该词汇表链接，其含义就被**编码进了规格说明书本身**——两种措辞都会路由到同一个量——随后 Z3 就会证明真正的冲突：≤30 ∧ ≥60 是无法同时满足的。它会报告 `FND_NUMERIC_CONTRADICTION` 并点名这两项需求。 这就是“神经符号 (neurosymbolic)”在本文中的含义：神经组件（用于判断语义的 embedding）永远只能**建议**两种措辞的含义；而由人类或 agent 将该含义**提交**为永久性的词汇表或反义词条目；只有在此时，数学上绝对可靠的逻辑层才会利用它来做出决定。语义因此变成了*文档中的数据*，而不是工具在背地里做出的猜测——所以相同的输入每次都会得到相同的答案。 同样的机制还可以桥接对立词（`antonym add seal expose` 会将“密封记录”和“公开记录”折叠为极性相反的同一个原子）以及普通的同义替换（“issue a token”与“grant a credential”）。你只需一次确定好词汇表，剩下的由 symspec 为你维持秩序。 ## 诚实的判定结果——`verified: false` 与任务清单 symspec 是围绕一套工作流而构建的：**由一个 agent（或人类）不断迭代规格说明书，直到它真正通过认证。**`check --strict` 是门禁，`data.verified` 是结论，而 `data.coverage.demotions` 就是任务清单。 `verified: true` 是一项刻意设定得极其*严格*的声明。它绝不意味着“没发现冲突”。它意味着证明器确实验证了整个文档： 1. **每一项需求都参与其中**——它与至少一个同级需求共享词汇，因此证明器确实对它们进行了比较。如果一项需求使用的是只有自己才懂的私有词汇，那它就像一座孤岛，而孤岛正是矛盾最容易藏身的地方。 2. **每一对潜在的冲突组合都经过了筛查**——当两项需求对同一个对象施加了不同的动词时，symspec 会将它们标记出来供你提议；在你做出决定（执行 `antonym add`、`glossary add` 或 `waive`）之前，本次运行将不会通过认证。 3. **确实发生了跨需求的比较**，并且语义层也已启动。只要以上任何一点未能达成，`verified` 就会是 `false`，`--strict` 的退出码就是 `3`，并且每一个原因都会出现在 `data.coverage.demotions` 中，**并附带能够解决该问题的确切命令**： ``` "coverage": { "encoded": 12, "excluded": 0, "pairsCheckedNote": "…why a low pair count is expected here…", "demotions": [ { "reason": "quantity-alias-candidate", "requirementIds": ["45defae7-…", "20aa64dc-…"], "action": "If both bounds constrain one quantity, run `symspec glossary add \"…\" \"…\"` so the numeric tier can prove any conflict; otherwise waive." } ] } ``` 因此，这个收敛过程完全是机械化的，中间无需人工介入： ``` check --strict # exit 3 — verified: false → read coverage.demotions → apply the listed ops (glossary add / antonym add / waive) or rewrite the named requirements to align vocabulary check --strict # repeat… → exit 0, verified: true — or exit 1 with a PROVEN contradiction the vocabulary alignment just exposed ``` 有一项原则主宰着这一切——**只做降级 (demotion-only)**：模糊的信号（embedding 相似度、覆盖盲区、未筛查的提议）只能将 `verified` 推向 `false`（即发出警报），但只有确定性的证明层才能给出“一切正常”的最终通行证。 **覆盖范围评估是显式的，绝不静默。** 因 error 级别的 lint 错误而被证明器跳过的一项需求，会引发一个顶级的 `FND_EXCLUDED_FROM_FORMAL` 警告，并将 `verified` 降级——对一项未被检查的需求保持沉默，绝不能被视为健康证明。你可以通过修复 lint 问题，或者通过豁免那个*阻塞性*的发现（`symspec waive add --ref `）来重新接纳该需求，使其重返求解器；仅仅豁免提示信息本身是无法恢复覆盖范围的。而对于那些任何可靠的提取器都无法从纯文本中恢复的内容——聚合/守恒求和、跨量算术、突发的结构性逻辑悖论——系统同样不会直接予以放行：`check` 会通过 `FND_RELATIONAL_UNCHECKED` 标记出这种*形态*并予以降级，所以“已验证”的状态绝对不会超出实际被比对过的范围。 ## 实战检验——对抗性测试循环 symspec 经历过真正的红蓝对抗评估，而不是仅仅做一场营销演示。 一个前沿大模型（Opus 4.8）作为“出题者”编写了包含真正具备机器可证明矛盾的需求规格说明书——并在盲审专家组和作为权威裁判的 Z3 的监督下——试图诱导 symspec 认证它们毫无问题。早期的 symspec 在 30 道题中**陷入了 25 个陷阱**。经过第一轮强化后，成绩变成了 **28/30**；而最后那些漏网之鱼都隐藏在数值层的结构性盲区中——例如与动词短语绑定的边界、从未被求和的聚合量，或者任何词典都无法触及的突发性逻辑悖论。[GitHub issue #2](https://github.com/theagenticguy/symspec/issues/2) 以一种唯一可靠的方式解决了它们：**每一次逃脱要么变成一个被*证明*的矛盾**（当可靠的提取器能够触达它时——就像上面输液泵的例子一样），**要么变成一次*诚实的降级***——即返回 `verified: false` 并附上使其具备可证明性的确切命令——这发生在没有任何可靠提取器能够触达它的时候。 目前，每一轮获胜的记录都被固化为回归测试用例：在 `adversarial/eval-rounds.ts` 中共有 **12 轮对抗，13 个通过的测试**。证明轮次会断言矛盾被触发并点名植入的罪魁祸首；而弃权轮次则会断言加固后的 `verified` 会因为*具备可操作性的原因*进行*降级*，而不是去认证一个谎言。该评估最初的获胜条件——在隐藏矛盾的情况下获取无误的认证——现在在每一个被固化的轮次中都已变得无法实现。 除此之外，一个**生成式对抗测试套件**（`adversarial/generate.ts`）会持续跨五个缺陷类别生成越来越隐蔽的规格说明书，并根据 Z3 的真实基准检查 symspec 的判定结果，从而确保随着代码的演进，检查器始终保持诚实可靠。 ## 引擎矩阵 symspec 将一个快速且**完全可重复**的核心与一个可选的“智能”层配对，该智能层只能进行*建议*——永远不能做出最终决定。对同一份文档运行两次，你会得到完全相同的答案。下表中的每一行代表一个检查引擎；“证明 (proves)”意味着数学上的保证，而不是一种启发式的猜测。 | 引擎 | 捕捉内容 | 现方式 | |---|---|---| | **句子解析器** | 将文本转化为清晰的需求，或者解释需要进行怎样的重写 | 优先进行模式匹配；只有在遇到复杂的句子时才会调用语言解析器 | | **写作质量 lint** | 损坏的交叉引用、循环链接、缺失的部分，以及 24 条行业标准写作规则 | 基于 INCOSE 编写的*《需求编写指南》*；每一个标记都包含引发问题的文本范围及其修复方法 | | **逻辑检查器** *(核心)* | 无法同时成立的两项需求；导致另一项需求冗余的需求；永远无法触发的规则 | 在进程内运行 **Z3** 定理证明器——无需额外安装——展示每一次判定背后的最小原因 | | **数值检查器** | 冲突的限制，例如针对同一测量指标的“2秒以内”与“3秒以上” | 使用相同的证明器，针对算术逻辑进行推理 (LIA/LRA) | | **时序检查器** *(选启)* | 顺序与时序上的冲突，例如“过热时，打开阀门”对比“控制器不得打开阀门” | 将时序规则转化为在有界时间轴上进行测试的逻辑表达式 | | **歧义检查器** | 模糊的词汇、产生两种理解方式的“和/或”、没有明确指代对象的代词 | 固定检测器；针对那些真正需要主观判断的歧义，会标记给人类或 agent 处理，绝不暗中猜测 | | **语义相似度层** *(核心，默认开启)* | 隐藏在不同措辞背后的冲突，以及证明器目前还无法识别的潜在反义词 | 一个在**本地**运行的小型语言模型负责*提供建议*；由你通过 `glossary add` / `antonym add` 进行确认，然后由逻辑检查器证明冲突。如果模型缺失，将导致运行失败，而不是跳过该检查层 | | **覆盖范围记账器** | 证明器从未进行过比对的需求，以及未经筛查的建议 | 确定性的参与度统计；任何未被覆盖的内容都会在 `coverage.demotions` 中给出修复建议并导致 `verified` 降级 | | **形式化证书** *(选启)* | 针对整个规格说明书的可复核证明工件 | **Lean 4** 证明助手；任何人随后都可以独立验证此文件 | 将这一切紧密联系在一起的一条准则是：**任何可能阻塞你的构建的内容，都可以从文档加上少数几个固定且受版本控制的输入中完全复现。**那个唯一的“智能”层会在每次检查时运行，但它只能提供建议；它的决定会由人类或 agent 进行审查，并保存到项目中（如 `glossary`、`antonyms`、`waivers`），从而让它们永远不再发生变化。 从数字上看：**20 条命令**，**75 个稳定的结果代码**（21 个错误代码，24 个 lint 代码，30 个发现代码）——它们只增不减，绝不重命名或删除——因此基于它们构建的自动化流程可以持续稳定工作；具备自我描述能力的 `manifest`，无处不在的结构化输出，为受 token 限制的 agent 准备的紧凑型 `--dense` 模式，以及上述提到的对抗性测试套件。 ## 专为 Agent 驱动而生 symspec 旨在由编码 agent 驱动，而不是从人类的笔触中随意抓取。完整的命令参考、参数 schema 和代码目录位于 [`docs/`](docs/README.md) 和 `symspec manifest` 中——以下是使其接口对 agent 友好的原因： - **`manifest`** — 一次调用就能以 JSON 格式返回整个工具的全貌：每一条命令、按命令划分的参数 schema（源自运行时校验所用的 Zod 字段）、稳定的代码目录、诚实声明的适用范围、被认可的数值单位，以及动态的 `backends` 报告（z3-wasm、外部 `z3`/`cvc5`、Lean）及其确切的版本号。只需获取一次，随后即可无需试错地直接驱动。 - **强类型信封** — 每一次成功返回的都是 `{ apiVersion, type, data }`；每一次失败返回的都是 `{ apiVersion, type: "error", error, code, suggestions, partial? }`。Agent 可以基于 `apiVersion` 进行版本协商，并统一根据 `type` 进行逻辑分支切换。 - **稳定的代码** — `ERR_*`、`FND_*` 和 `GTWR_*` 是导出的 Zod 枚举，每一个都带有独立的描述，且为只增不减模式（快照测试会防止其被重新编号或删除）。manifest 中的代码表正是派生自这些相同的枚举，从而保证输出方与文档之间绝不会发生偏离。 - **`--field`** — 类似 jq 风格的 JSON 信封投影，使得 agent 可以直接精准提取诸如 `data.verified` 或 `data.coverage.demotions` 的数据，而无需完整的 JSON 解析器。 - **`--dense`** — 节省 token 的输出模式：经过压缩、剔除了默认/空值键名、省略了冗长的证据（传递 `--evidence` 可保留证据）；保持相同的 schema，且可循环还原。 - **退出代码** — `0` 表示无误，`1` 表示发现了阻塞性问题，`2` 表示操作失败，`3` 表示严格的覆盖率门禁被触发。输出的标志位永远不会改变退出代码。 - **可导入的库** — CLI 只是 `src/index.ts` 外层的一层薄薄的格式化器：`import { applyChange, analyze, runCheck, checkGtWRules, atomize } from 'symspec'`。 - **`AGENTS.md`** — agent 集成指南，由驱动 `manifest` 的相同描述语料库自动生成，因此它能与实际的命令接口保持完全同步。 你可以利用 `symspec apply` 通过一次安全的操作构建出完整的规格说明书：将一批编辑操作作为单一的全部成功或全部回滚事务进行应用，在此过程中使用可向前引用的人类可读键名（如 `G1`、`AUTH-3`），这些键名会在永久的 ID 生成之前被解析。如果其中任何一个步骤无效，则什么都不会保存，并且系统会告诉你哪一行出了错。 ## 深度解析工作原理 若要了解完整的流水线——包括以正则优先的解析阶梯、原子化处理与反义词表、Z3 编码与 unsat core（无法满足的核心）提取、数值/时序/歧义判定层、本地 ONNX 语义层以及可选的 Lean 4 证书，请查阅 [`docs/`](docs/README.md) 下生成的文档树：其中包含了模块结构图、数据流和时序图、公共 API 与 CLI 参考手册、契约关系图以及调试指南，所有内容均关联到了具体的源码。 其整体形态如下：symspec 运行着一个**强制执行的流水线**——`parse → lint → check → certify`——这种执行顺序是承重墙级别的关键。如果一个陈述在早期的表层阶段未能通过检查，它就会被*排除*在形式化阶段之外（将未解析的或存在悬空引用的文本送入 SMT 编码是不靠谱的），而且这种排除行为会被明确报告出来，绝不静默处理。形式化阶段是**相对于原子化而言可靠的**：每一处被报告的冲突都是真实的；而被漏掉的冲突则隐藏在互不匹配的词汇背后——这正是语义层以及提议/决定（propose/decide）循环存在的意义，旨在将其挖掘出来。 ## 开发说明 ``` pnpm install # from lockfile pnpm build # tsdown → dist/ (library + CLI entry, with .d.ts) pnpm cli # run the CLI from source without building (tsx) pnpm test # vitest run pnpm check # full gate: biome ci + tsc --noEmit + vitest run + knip pnpm gen:agents # regenerate AGENTS.md from the manifest (check:agents guards drift) ``` **质量门禁。** `pnpm check` 是合并代码的门禁；四个子检查中的任何一个返回非零退出码都会被视为阻塞项。在修改了命令描述或 manifest 之后必须执行 `pnpm gen:agents`——AGENTS.md 的偏离会导致测试失败。 **求解器。** 默认的 `check` 只需要打包好的 `z3-solver` WASM 依赖包即可运行。可选的外部二进制程序已固定在 `mise.toml` 中（默认处于注释状态）：用于 `--solver` 交叉验证的 `z3`/`cvc5`，以及用于 Lean `certify` 认证层的 `elan`。 该项目还将其来之不易的经验教训保留在代码仓库的 `.erpaval/` 目录下（包括设计恒量、工具边缘情况、agent 工作流的陷阱），并在会话开始时呈现给 Claude Code，从而让这些知识伴随代码一同传播。 ## 词汇表 上文所使用术语的通俗语言定义。 | 术语 | 含义 | |---|---| | **Agent（编码 agent）** | 编写和修改代码及规格说明书的 AI 助手——例如 Claude Code、Cursor、Codex——通常是通过代表你运行诸如 symspec 之类的命令来实现。 | | **规格说明书 (Spec) / 需求 (Requirement)** | 对系统必须执行操作的单项陈述（*“当用户登录时，系统应当发放一个 token”*）。规格说明书则是这些需求的集合。 | | **EARS** | *Easy Approach to Requirements Syntax（需求语法简易方法）*。一套小型的句子模板集合（包括 ubiquitous 无条件必然、event-driven 事件驱动、state-driven 状态驱动、optional-feature 可选特性、unwanted-behavior 非期望行为），旨在让需求保持清晰统一。 | | **INCOSE GtWR** | 国际系统工程师委员会发布的*《需求编写指南》(Guide to Writing Requirements)*——这是一项行业标准的写作准则。symspec 会自动检查其中的 24 条规则。 | | **形式化 / “证明”** | 以数学为后盾的结果，绝非猜测。如果 symspec 指出两项需求相矛盾，那是因为求解器证明了这一点；而“无误”的结果仅仅意味着没有*证明*出冲突，并不代表该规格说明书完美无缺。 | | **SMT** | *Satisfiability Modulo Theories（可满足性模理论）*——symspec 所使用的求解器类别。它会回答“是否存在让所有这些陈述同时成立的方法？”如果不存在，它会给出原因。 | | **Z3** | symspec 运行的特定 SMT 求解器，已被编译为 WebAssembly，因此无需额外安装任何东西。 | | **无法满足的核心 (Unsat core)** | 已经存在冲突的最小需求子集——这正是 symspec 能够准确指出罪魁祸首的原因，而不仅仅是告诉你“某些地方有问题”。 | | **神经符号** | 将神经/模糊组件（判断语义的 embedding）与符号/逻辑组件（SMT 证明器）相结合。在这里，神经组件负责*提议*，而符号组件负责*决定*。 | | **原子 / 原子化** | 逻辑检查器进行比较时所参照的需求动作的标准化规范形式（例如“授予访问权限”）。当两项需求的原子相匹配但极性（做与不做）相反时，它们就会发生冲突。 | | **提议 / 决定** | 承重级别的分离设计：模糊信号只能*提议*词汇间的联系；只有通过提交归档的工件再加上可靠的证明器才能对最终判定做出*决定*。 | | **降级** | 指覆盖盲区或未筛查的提议将 `verified` 状态推向 `false` 的过程。模糊信号只能导致降级（降低置信度），而永远不能升级（通过认证）。 | | **反义词表** | symspec 精心维护的相反动词对列表（如授权↔拒绝、密封↔暴露等），它让证明器能够将“授予访问权限”和“拒绝访问权限”识别为极性相反的同一项声明。该表仅能通过显式编辑或你确认的 `antonym add` 命令来扩充。 | | **词汇表 (Glossary)（在 symspec 中）** | 已保存并提交到文档中的确认过的同义词列表——这是你用来永久性地告诉工具“这两种措辞意思相同”的方法。 | | **覆盖范围** | `data.coverage` 会报告证明器实际对哪些需求进行了比较，以及还有哪些项尚未经过筛查。任何盲区都会导致 `verified` 被降级。 | | **相对于原子化而言可靠** | 一种精确且诚实的保证：每一处报告的冲突就*需求的原子化结果而言*都是真实的；冲突依然可能隐藏在不匹配的词汇背后，因此沉默并不等于认证合格。 | | **LIA / LRA** | *Linear Integer / Real Arithmetic（线性整数/实数算术）*——求解器用于捕捉诸如“2秒以内”与“3秒以上”之类冲突限制的数值推理方式。 | | **LTL / sound-for-UNSAT** | *线性时序逻辑 (Linear Temporal Logic)* 用于表达时序/顺序规则；时序检查器具备 sound-for-UNSAT 特性——被报告的冲突是真实的，但在有界时间窗口内无误的运行结果并不能代表完全的保证。symspec 会在输出中明确标示这一点。 | | **Lean 4** | 一款*证明助手*——用于验证证明的软件。symspec 可以选择性地生成一个任何人都能独立复核的 Lean 证明工件。在执行 `check` 时绝非必须项。| **清单** | 一条命令 (`symspec manifest`) 即可将整个工具以结构化数据的形式描述出来，让 agent 通过一次调用就能掌握所有的命令和选项。 | | **JSON 信封** | 每一条命令都会返回的统一结构：成功时为 `{ apiVersion, type, data }`，失败时为 `{ …, code, suggestions }`。 | | **结果代码** | 用于表示发现或错误的简短且稳定的标识符（如 `FND_CONTRADICTION`、`ERR_DOC_NOT_FOUND`）。只增不改。 | | **豁免** | 出于记录在案的原因而刻意将特定的发现搁置一旁，以免特意为之的选择充斥在未来的每一次审查中。 | | **确定性 / 可复现性** | 相同的输入总能产生相同的输出。symspec 确保每一个会阻塞构建的结果都具备确定性，从而使结果绝不会在不同运行或不同机器之间发生偏离。 | | **CI** | *持续集成*——在每次代码变更时运行检查的自动化流水线。symspec 的退出状态可以直接接入其中。 | | **WebAssembly (WASM)** | 一种可移植的格式，能够让诸如 Z3 之类的软件在任何环境中运行而无需单独安装。 |