minicheck-mcp

一个作为 MCP 服务器的模型检查器。让代理验证状态机，而不是猜测。

为什么存在

代理不断设计状态机——重试循环、锁协议、会话生命周期、子代理之间的交接——然后用文字推理正确性。关于并发的文字推理对模型和对人一样会失败：考虑那些想到的交错，却漏掉了没想到的那个。

拥有决策过程的代理不必猜测。它得到裁决，当属性失败时，得到破坏它的确切步骤序列——这也是修复设计而非道歉所需的东西。

它发送的规范是数据，绝不是代码，因此代理提交的任何内容都不会被执行——返回的是带有最短反例轨迹的裁决。

Related MCP server: agent-gate

安装

# from GitHub (PyPI release pending)
pip install "minicheck-mcp @ git+https://github.com/nickharris808/minicheck-mcp.git"
pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git"  # + the MCP SDK

pip install minicheck-mcp 目前还不行——该包不在 PyPI 上。按上面所示从 GitHub 安装；这会自动拉取 minicheck。python build_pypi.py 会生成一个可上传到 PyPI 的构件，供两个包发布时使用（PyPI 拒绝此包使用的直接依赖引用，该引用是为了在没有索引的情况下保持可安装性）。

然后注册它（claude_desktop_config.json，或任何 MCP 客户端）：

{ "mcpServers": { "minicheck": { "command": "minicheck-mcp" } } }

仓库将此作为 mcp.json 提供。

30 秒快速入门

问代理：“我有一个重试循环，递增计数器直到成功。检查它不能重试超过 3 次。” 它向 check_invariant 发送此规范：

{
  "name": "retry",
  "fields": ["tries", "done"],
  "initial": {"tries": 0, "done": 0},
  "transitions": [
    {"label": "attempt", "when": {"done": 0}, "set": {"tries": {"incr": 1}}},
    {"label": "succeed", "when": {"done": 0}, "set": {"done": 1}}
  ],
  "invariants": {"bounded_retries": {"forbid": {"tries": 4}}}
}

并得到——用 python -c "from minicheck_mcp import dispatch; import json; print(json.dumps(dispatch('check_invariant', {'spec': SPEC}), indent=2))" 重现：

{
  "ok": true,
  "reachable_states": 129,
  "exhaustive": false,
  "invariants": {
    "bounded_retries": {
      "holds": false,
      "counterexample": [
        {"label": null,      "state": {"tries": 0, "done": 0}},
        {"label": "attempt", "state": {"tries": 1, "done": 0}},
        {"label": "attempt", "state": {"tries": 2, "done": 0}},
        {"label": "attempt", "state": {"tries": 3, "done": 0}},
        {"label": "attempt", "state": {"tries": 4, "done": 0}}
      ],
      "steps": 4
    }
  },
  "incomplete_reason": "IntBoundExceeded: transition 'attempt' drives field 'tries' to 65, outside int_bound 64. The state space is not finite under this bound, so no exhaustive verdict is available. Re-run with int_bound >= 65.",
  "advice": "the state space was not fully explored, so any invariant not refuted below is UNDETERMINED (null), not proved. Raise int_bound or add a 'when' guard that bounds the growing field, then check again.",
  "all_hold": false,
  "verdict": "REFUTED",
  "verdict_means": "a counterexample was found; it starts at the initial state and replays"
}

不是“这可能永远循环”——而是破坏它的确切四步。

不过，请完整阅读回复，这个快速入门正是原因：exhaustive 是 false。反驳仍然成立——反例自带见证，且该轨迹可重放——但此规范中的其他内容均未确立，因为 attempt 没有守卫，并将 tries 推过 int_bound。反驳只需一个见证；证明需要整个空间。

教程——一次会话实际的样子

代理编写了一个会话生命周期，想知道会话关闭后是否还能被使用。以下是整个交流过程。

1. 代理询问格式（spec_help），然后发送 check_invariant：

{
  "name": "session",
  "fields": ["state", "used"],
  "initial": {"state": 0, "used": 0},
  "transitions": [
    {"label": "open",  "when": {"state": 0}, "set": {"state": 1}},
    {"label": "use",   "when": {"state": 1}, "set": {"used": 1}},
    {"label": "close", "when": {"state": 1}, "set": {"state": 2}},
    {"label": "reopen","when": {"state": 2}, "set": {"state": 1}}
  ],
  "invariants": {"no_use_after_close": {"forbid": {"state": 2, "used": 1}}}
}

2. 它得到带有确切路径的反驳：

{
  "ok": true,
  "verdict": "REFUTED",
  "exhaustive": true,
  "reachable_states": 5,
  "all_hold": false,
  "invariants": {
    "no_use_after_close": {
      "holds": false,
      "steps": 3,
      "counterexample": [
        {"label": null,    "state": {"state": 0, "used": 0}},
        {"label": "open",  "state": {"state": 1, "used": 0}},
        {"label": "use",   "state": {"state": 1, "used": 1}},
        {"label": "close", "state": {"state": 2, "used": 1}}
      ]
    }
  }
}

所写的这个不变式禁止曾经使用过已关闭的会话，这不是代理的意思——它指的是“关闭时没有 use 转换”。反例使差异具体化，而不是留待一段听起来合理的段落。

3. 代理修复模型并重新运行。 used 应表示“自本次会话打开以来使用过”，因此 close 清除它：

{"label": "close", "when": {"state": 1}, "set": {"state": 2, "used": 0}}

{"ok": true, "verdict": "PROVED", "exhaustive": true, "reachable_states": 4, "all_hold": true}

PROVED 和 exhaustive: true 是应成对阅读的。前者不能在没有后者的情况下发出，但检查两者使习惯明确——而正是这个习惯在规范超出界限的那天保护你。

4. 代理绝不能做的事。 如果回复是 "verdict": "UNDETERMINED"，那不是通过。这意味着搜索提前停止——阅读 incomplete_reason 和 advice，限制增长字段，然后再次询问。如果 ok 为 false，则根本不存在裁决，且 all_hold 为 null。

工具

规范格式

{
  "name": "mutex",
  "fields": ["a", "b", "lock"],
  "initial": {"a": 0, "b": 0, "lock": 0},
  "transitions": [
    {"label": "a_enter", "when": {"a": 0, "lock": 0}, "set": {"a": 1, "lock": 1}},
    {"label": "a_exit",  "when": {"a": 1},            "set": {"a": 0, "lock": 0}}
  ],
  "invariants": {"not_both": {"forbid": {"a": 1, "b": 1}}},
  "goal": {"require": {"a": 1}}
}

when 是 field == value 测试的合取（省略则始终启用）。set 赋值一个字面量，或对整数使用 {"incr": n} / {"decr": n}。不变式是 {"forbid": {...}}（当每个列出的字段匹配时失败）或 {"require": {...}}（除非它们匹配，否则失败）。

整数是有界的，且边界会被检查——int_bound（默认 64）是字段可持有的最大幅度。会使字段超出边界的运行会停止并报告 exhaustive: false，而不是饱和该值，因为静默截断的搜索会为从未访问过的状态报告“成立”。参见诚实范围了解如何解读结果裁决。

为什么声明式

一个 exec 代理提供的 Python 的 MCP 服务器将是一个带额外步骤的远程代码执行漏洞。这里的规范是数据：看起来像 __import__('os').system(...) 的字段值保持为字符串，并作为字符串比较。有一个测试正是断言这一点。

没有 SDK？仍然可用。

工具是普通函数。dispatch 是传输层使用的同一入口点，因此你可以从脚本或测试中调用它，而无需代理参与：

from minicheck_mcp import dispatch
dispatch("check_invariant", {"spec": my_spec})

如果没有安装 mcp，minicheck-mcp 会打印一个 JSON 错误，说明如何安装它，并以非零状态退出，而不是回溯。

诚实范围

将裁决视为三值。 这是对代理最重要的部分，因为代理读取字段并据此行动，而不是对段落进行判断。

每个响应还携带 verdict_means，一行解释，代理可以逐字引用给用户，而不是转述（并可能软化）它。

每个响应都显式携带 all_hold 和 holds，包括错误。早期版本在失败时省略它们，因此 result.get("all_hold") 在崩溃和真正的未确定结果时都返回 None——两者都是假值，恰好像反驳。

当 exhaustive 为 false 时，响应还携带 incomplete_reason 和 advice，指出要更改的内容。当不变式被平凡满足时，会出现 warnings 数组——它确实成立，但验证不了任何东西。

它证明了什么。 一个有限的声明式状态机在声明的边界内，是否满足关于每个交错的不变式。

它不证明什么。

• 关于你的实现——只关于你发送的规范。规范是抽象。

• 超出 int_bound（默认 64）或 200,000 状态上限的任何内容。超出任一都会产生 UNDETERMINED，绝不会静默通过。

• 关于 AG-EF 之外的活性，以及 LTL 中的任何内容。

规范中的任何内容都不会被执行。 规范是数据：字段名、字面量和比较。没有 eval，没有 exec，也没有将规范中的字符串变成可调用对象的代码路径。这就是声明式加载器存在而不是接受 Python 的原因。

这里没有的东西

这是引擎和调用它的安全方式。维护的危险属性语料库、发现仅当两个组件组合时才存在的危险的组合分析，以及使裁决事后可审计的证据链，是商业产品。此服务器是 MIT 许可，并保持如此。

故障排除

ok: false, error: "SpecError"。 规范格式错误，消息指出键。先调用 validate_spec，或 spec_help 获取带工作示例的格式。

verdict: "UNDETERMINED" 在我预期通过的规范上。 搜索未覆盖整个状态空间——通常是一个无界增长的字段。阅读 incomplete_reason 和 advice。添加一个阻止增长的 when 守卫。不要将其视为通过。

ok: false, error: "BadArguments"。 工具被调用时带有它不接受的参数。每个工具都接受 spec；check_invariant 还接受可选的 invariant 名称。

check_liveness 上 ok: false 且 "spec declares no 'goal'"。 活性需要可到达的目标。添加一个与不变式形状相同的 goal 块。

出现 warnings 数组且不变式仍说 holds: true。 不变式命名了一个有界空间无法表示的值，因此它因与你的协议无关的原因而满足——通常是字面量中的拼写错误，或 int_bound 低于你打算禁止的值。

服务器立即退出并显示 JSON 错误。 未安装 MCP SDK：pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git"。工具仍可通过 from minicheck_mcp import dispatch 导入和测试，无需它。

我的代理将错误视为“属性没问题”。 它不应该能够：每个响应都显式携带 all_hold 和 holds，且任何错误时两者都是 null，同时还有 verdict: "ERROR"。首先根据 result["ok"] 分支。

性能

受底层检查器限制。规范以声明式到达这里，这是检查器的编译路径——在 M 系列笔记本电脑上的 CPython 3.11 中约为 2.5×10⁵–7.5×10⁵ 状态/秒，可通过在 minicheck 仓库中运行 python bench.py 重现。适合几万状态的规范在远不到一秒内回答。服务器层本身没有测量到的瓶颈——它是一个薄分发层。

常见问题

"从语言模型运行 spec 会不会让它执行代码？" 不会，这正是声明式格式存在的原因。spec 是数据：字段名、字面量和相等性比较。没有 eval，没有 exec，也没有任何代码路径会把 spec 中的字符串变成可调用对象。看起来像 __import__('os').system(...) 的字段值仍然是一个字符串，并作为字符串进行比较。有一个测试专门断言这一点，对抗性测试套件会向每个工具发送代码形态的载荷。（minicheck 的 Python Model API 不同——那是代码，来自它的不受信任模型应当得到与任何不受信任的 Python 相同的谨慎对待。本服务器不暴露它。）

"为什么不直接让 agent 编写 Python 并运行它？" 一个对 agent 提供的 Python 执行 exec 的 MCP 服务器，就是一个多绕了几步的远程代码执行漏洞。声明式格式牺牲了表达能力，换来的是一个可以用一句话说清并且可测试的性质。

"我的 agent 读取了 all_hold 并断定属性没问题，但实际上有错误。" 它不应该能做到这一点：每个响应都显式携带 all_hold 和 holds，在出错时两者都是 null，同时还有 verdict: "ERROR" 和 ok: false。早期版本在失败时省略了它们，因此 result.get("all_hold") 在崩溃和真正未确定的结果下都返回 None——而两者都是假值，与反例完全一样。先判断 result["ok"]，再判断 verdict，永远不要依赖 all_hold 的真值。

"为什么每个回复里都有一个 verdict_means 字符串？" 因为 agent 转述结论时往往会软化它，"检查没有定论"经过两轮转述就变成了"看起来没问题"。verdict_means 是一行解释，agent 可以逐字引用给用户。

"UNDETERMINED——agent 应该重试，还是报告成功？" 默认两者都不做。它表示搜索提前停止，因此没有确立任何结论。请阅读 incomplete_reason 和 advice，它们指出了需要修改的内容——通常是一个无界增长的字段。给它加上边界再重新询问。把它报告为通过，正是整个包所要对抗的失败模式。

"我需要 MCP SDK 吗？" 只有在通过传输层提供服务时才需要。工具本身就是普通函数：from minicheck_mcp import dispatch 与传输层使用的入口点相同，因此你可以在没有 agent 参与的情况下从脚本或测试中调用它。如果没有安装 mcp，minicheck-mcp 命令会打印一条 JSON 错误信息说明如何安装，并以非零状态退出，而不是抛出 traceback。

"它可以用于生产环境吗？" 可以，并且经过了全面测试——但周围的 agent 生态发展很快，因此 MCP 接口是最可能需要升级版本的部分。底层的检查器是 minicheck，并且是稳定的。

"这里的东西给了我一个自信但错误的答案。" 这值得提交一个 issue 而不是绕开它；请附上 spec。从面向 agent 的服务器可达的虚假 holds: true 是这个包可能拥有的最严重的 bug，而恰好有一个这样的 bug 在 minicheck 0.1.0 中被发现、修复并披露。

Tests

pip install -e ".[test]" && pytest

$ pytest -q
........................................................................ [ 74%]
.........................                                                [100%]
100 passed in 2.31s

102 个测试，每个工具都经过真实的 dispatch 路径，包括畸形输入、未知工具以及不执行代码的保证。其中一个测试用 pytest --collect-only 断言本 README 自身的测试数量，因此徽章不会漂移。

The portfolio

一个理念贯穿所有项目：你无法检查的结论不是结论——以及它的推论，支配着这里的每一个表面：未确定不等于通过。

在浏览器中试用 · 对状态机进行模型检查 · specforge 排行榜

基准真值数据 · protocol-bench · specforge

The commercial offering

这些是引擎。没有开源的，是让它在规模化时真正有用的部分：持续维护的危险属性语料库、能够发现只有两个组件组合时才存在的危险的组合分析、信任模型敏感性扫描，以及让结论事后可审计的证据链。上面的工具都是 MIT 许可，并且会一直保持。

Documentation

完整文档，包括概念指南以及与 TLA+、SPIN、Alloy 和 CBMC 的诚实对比，位于 https://nickharris808.github.io/verification-docs/。

Contributing

欢迎提交 bug 报告和 pull request——请参阅 CONTRIBUTING.md。这个工具判断错误的反例，是你能发送的最有用的东西。

Citing

引用元数据位于 CITATION.cff；GitHub 会据此渲染一个 Cite this repository 按钮。

Licence

MIT。请参阅 LICENSE。