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"
}

「無限ループするかもしれません」ではなく、それを破る正確な4つのステップです。

ただし、返信全体を読んでください。このクイックスタートがその理由です：exhaustive は false です。反駁はそれでも成立します——反例はそれ自体が証人を伴い、そのトレースは再生可能です——しかし、この仕様の他の部分は何も確立されていません。なぜなら attempt にはガードがなく、tries を int_bound を超えて駆動するからです。反駁には1つの証人で十分ですが、証明には空間全体が必要です。

チュートリアル——実際のセッションの様子

エージェントはセッションのライフサイクルを書き、セッションが閉じられた後に使用できるかどうかを知りたいと思っています。以下がやり取り全体です。

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 を報告します。なぜなら、静かに切り詰められた検索は、訪れたことのない状態について「成立」と報告するからです。結果の判定結果の読み方については誠実な範囲を参照してください。

なぜ宣言的か

エージェントが提供したPythonを exec するMCPサーバーは、余計な手順が付いたリモートコード実行の穴になります。ここでの仕様はデータです：__import__('os').system(...) のように見えるフィールド値も文字列のままであり、文字列として比較されます。まさにそれを検証するテストがあります。

SDKなしでも使用可能。

ツールは単純な関数です。dispatch はトランスポートが使用するのと同じエントリーポイントなので、エージェントを介さずにスクリプトやテストから呼び出すことができます：

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

mcp がインストールされていない場合、minicheck-mcp はトレースバックを出力する代わりに、インストール方法を説明するJSONエラーを出力して非ゼロで終了します。

誠実な範囲

判定結果は3値として読んでください。 これはエージェントにとって最も重要な部分です。なぜなら、エージェントは段落に判断を委ねるのではなく、フィールドを読んでそれに基づいて行動するからです。

すべての応答には verdict_means も含まれます。これはエージェントが言い換え（そしておそらく和らげる）のではなく、そのままユーザーに引用できる1行の説明です。

すべての応答には、エラーを含めて 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を受け入れるのではなく宣言的ローダーが存在する理由です。

ここにないもの

これはエンジンと、それを安全に呼び出す方法です。保守されたハザードプロパティコーパス、2つのコンポーネントを組み合わせたときにのみ存在するハザードを見つける合成分析、そして判定結果を後から監査可能にする証拠の記録は、商用製品です。このサーバーは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 でSDKなしでもインポートおよびテスト可能です。

エージェントがエラーを「プロパティは問題ない」と扱う。 それはできないはずです：すべての応答には all_hold と holds が明示的に含まれ、エラー時には両方とも null であり、verdict: "ERROR" が付随します。最初に result["ok"] で分岐してください。

パフォーマンス

基盤となるチェッカーによって制限されます。仕様は宣言的にここに届き、これはチェッカーのコンパイル済みパスです——Mシリーズのラップトップ上のCPython 3.11でおよそ2.5×10⁵〜7.5×10⁵状態/秒であり、minicheck リポジトリで python bench.py を実行することで再現できます。数万状態に収まる仕様は、1秒未満で応答します。サーバー層自体に測定されたボトルネックはありません——それは薄いディスパッチです。

FAQ

「言語モデルからスペックを実行すると、コードが実行されるのでは？」
いいえ、だからこそ宣言的フォーマットが存在します。スペックはデータです。フィールド名、リテラル、等価比較です。eval も exec も、スペック内の文字列を呼び出し可能なものに変えるコードパスもありません。__import__('os').system(...) のように見えるフィールド値は文字列のままで、文字列として比較されます。それを正確に検証するテストがあり、敵対的スイートはすべてのツールにコード形状のペイロードを送り込みます。（minicheck の Python Model API は異なります — それはコードであり、そこからの信頼できないモデルは、信頼できない Python と同様の注意を払う価値があります。このサーバーはそれを公開していません。）

「エージェントに Python を書かせて実行させればいいのでは？」
エージェントが提供した Python を exec する MCP サーバーは、余計な手順を踏んだリモートコード実行の穴になるでしょう。宣言的フォーマットは表現力を犠牲にし、一文で述べてテストできる特性を得ます。

「私のエージェントが all_hold を読んで、プロパティは問題ないと結論しましたが、エラーがありました。」
それはできないはずです。すべてのレスポンスは all_hold と holds を明示的に持ち、エラー時には両方とも null になり、verdict: "ERROR" と ok: false が付きます。以前のバージョンは失敗時にそれらを省略していたため、result.get("all_hold") はクラッシュ時も真の未確定結果のときも None を返し、どちらも偽値で、反証とまったく同じでした。result["ok"] を最初に分岐し、次に verdict で分岐してください。all_hold の真偽で分岐してはいけません。

「なぜすべての返信に verdict_means 文字列があるのですか？」
エージェントが判定を言い換えると、それを和らげる傾向があり、「チェックは決定的ではなかった」がさらに2ホップで「問題ないように見える」になります。verdict_means は、エージェントがユーザーにそのまま引用できる1行の説明です。

「UNDETERMINED — エージェントは再試行すべきですか、それとも成功を報告すべきですか？」
デフォルトではどちらでもありません。検索が早期に停止したことを意味し、何も確立されていません。incomplete_reason と advice を読んでください。それらは何を変更すべきかを示します — 通常は無制限に成長するフィールドです。それを制限して再度問い合わせてください。合格として報告することは、このパッケージ全体が対抗するように設計された失敗モードです。

「MCP SDK は必要ですか？」
トランスポート経由で提供する場合のみ必要です。ツールは単純な関数です。from minicheck_mcp import dispatch はトランスポートが使うのと同じエントリポイントなので、エージェントを介さずにスクリプトやテストから呼び出せます。mcp がインストールされていない場合、minicheck-mcp コマンドはインストール方法を示す JSON エラーを出力し、トレースバックを出す代わりに非ゼロで終了します。

「本番環境で使えますか？」
はい、完全にテストされています — ただし、周囲のエージェントエコシステムは急速に動くため、MCP サーフェスがバージョンアップを最も必要とする部分です。基盤となるチェッカーは minicheck で、安定しています。

「ここで何かが私に間違った自信のある答えを与えました。」
回避策ではなく issue を立てる価値があります。スペックを含めてください。エージェント向けサーバーから到達可能な誤った holds: true は、このパッケージが持ちうる最も深刻なバグであり、まさにその種のバグが minicheck 0.1.0 で発見され、修正され、開示されました。

テスト

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

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

102 のテスト、すべてのツールを実際の dispatch パスを通してテストし、不正な入力、未知のツール、コード非実行の保証を含みます。1つはこの README 自身のテスト数を pytest --collect-only に対して検証するため、バッジがずれることはありません。

ポートフォリオ

すべてに通じる1つの考え: 確認できない判定は判定ではない — そして、ここにあるすべての表面を支配するその系: 未確定は合格ではない。

ブラウザで試す · 状態機械をモデルチェック · specforge リーダーボード

正解データ · protocol-bench · specforge

商用提供

これらはエンジンです。オープンソースではないのは、大規模で有用にするものです: 維持されたハザードプロパティコーパス、2つのコンポーネントを組み合わせたときだけ存在するハザードを見つける構成分析、信頼モデル感度スイープ、そして後から判定を監査可能にする証跡です。上記のツールは MIT であり、そのままです。

ドキュメント

コンセプトガイドと TLA+、SPIN、Alloy、CBMC に対する正直な比較を含む完全なドキュメントは、https://nickharris808.github.io/verification-docs/ にあります。

貢献

バグ報告とプルリクエストを歓迎します — CONTRIBUTING.md を参照してください。このツールが誤って処理する反例は、送っていただける最も有用なものです。

引用

引用メタデータは CITATION.cff にあります。GitHub はそこから Cite this repository ボタンをレンダリングします。

ライセンス

MIT。 LICENSE を参照してください。