crs-mcp

あなたのパッチを書いたエージェントは、自分の宿題を採点できません。

今すぐ試す、インストール不要: ブラウザデモを開く そして Load a forgery を押してください — チェッカーはそれを拒否します、クライアントサイドで。

AIコーディングエージェントに、言い逃れできない判定面を与えるMCPサーバーです。エージェントはガードを提案しますが、このサーバーはそのガードが実際に健全かどうかを判断し、健全でない場合は具体的な反例を返します。

pip install "crs-mcp@git+https://github.com/nickharris808/crs-mcp@main"

プレリリース版。 PyPI名は予約済みで、公開は間もなくです。それまでは上記の行が動作するインストール方法です。CIでLinux、macOS、Windowsでテストされています。

30秒クイックスタート

Claude Desktop（claude_desktop_config.json）またはCursorに追加します:

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

次にエージェントに依頼します: "この読み取りの前に境界チェック 1 + payload <= record_len を追加しました。3 + payload <= record_len に対して認証してください。"

{
  "verdict": "PROVEN_UNSOUND",
  "summary": "The guard admits 509 state(s) the safety property forbids (out of 65,536). Example: {'record_len': 1, 'payload': 0}.",
  "detail": {
    "over_acceptance": 509,
    "box_volume": 65536,
    "counterexample": {"record_len": 1, "payload": 0},
    "hit_probability": 0.0077667236328125,
    "expected_draws_to_hit": 128.75442043222003
  }
}

これは実際の反例です: payload=0, record_len=1 ではガードは通過し、安全性プロパティは成立しません。エージェントはこれに反論できませんし、あなたもできません。

Related MCP server: Chiasmus

3つの判定

OUT_OF_SCOPE が重要です。これは失敗ではなく、そして強調して合格ではありません。エージェントは「エラーなし」を「承認」と読んでコミットするでしょう。ツールの説明はその読み方に対抗するように書かれており、explain_refusal は「これを承認として扱わないでください」と明確に述べた散文を返します。常に緑だけを返すツールは、ツールがないより悪いです。

ツール

verify_certificate はさらに certificate_verdict を返します。これは certkit 自身の ACCEPTED / REFUSED / UNVERIFIED です。チェックに失敗した証明書は OUT_OF_SCOPE として報告され、決して PROVEN_UNSOUND としては報告されません。悪い証明は証拠の欠如であり、不健全性の証拠ではありません。ガードが不健全であることを証明できるのは状態の数え上げだけであり、それが certify_guard の役割です。

decide_guard: 同じ答えを、より早く

ほとんどの場合、エージェントが尋ねるのは これは安全か? であり、どの程度安全でないか? ではありません。decide_guard は領域全体を数える代わりに、最初の逃げる状態で停止します。不健全なガードで測定した場合:

exploit-counter リポジトリ内の python benchmarks/decide_vs_count.py で再生成できます。そこが数え上げが行われる場所です。ギャップはボックスが大きくなるにつれて広がります。なぜなら数え上げは違反領域全体を列挙するのに対し、決定は最初の逃げる状態で停止するからです。

同一の判定 — テストは150のランダムな仕様でそれらが一致することを検証します。健全なガードはどちらの方法でも同じコストです。なぜなら健全性を確立するには完全な列挙が本当に必要だからです。

結果には over_acceptance フィールドは含まれません。何も数えていないので、そこにゼロでも数値を報告することは、分析が生成しなかった数値になるでしょう。

どのように決定するか、そして正直な限界

認証は、宣言したボックスに対する徹底的な整数数え上げによって行われます。これはそのボックスに対しては健全かつ完全です — そしてその外側については何も言いません。だからボックスは必須引数であり、文脈から推測されるものではありません。

カウンターは最も広い変数以外のすべての変数を列挙し、最も広い変数は閉形式で解きます。したがってコストは他の範囲の積であり、上限はその積に適用されます — ボックス体積ではありません。上限は500,000列挙ポイントです。このマシンで測定:

ミリ秒の列は1台のマシンからのもので、あなたのマシンでは異なります。python benchmarks/ceiling.py でこの表をあなたのマシンで再生成できます。体積、列挙数、判定は正確でマシンに依存しません。

上限内のすべての決定は0.25秒未満で完了するため、エージェント呼び出しが停止することはありません。これは以前は当てはまりませんでした。最悪ケースのプロファイリングでは、時間の約70%がPythonの Fraction 型内で費やされていました。そのため exploit-counter は、すべての係数が整数である場合（すべての境界関係がそうである）に整数のみの内部ループを実行するようになりました。整数は有理数の部分集合なので、これは同じ算術です — より高速な近似ではありません — そして test_integer_and_rational_paths_agree は2つの実装を相互にチェックします。

最も密な形状では 1,491.2 ms → 244.6 ms です。測定した3つの形状全体で中央値6.06倍、3.55倍–10.25倍が観測されました。形状ごとに11回のペア繰り返しで、毎回カウントはビット単位で同一です。make bench-fast-path で再生成できます。数値はこのページではなく、コミットされた artifacts/crs/bench_fast_path.json から来ています。中央値を引用してください — 範囲はマシンの負荷と問題の形状によって動くため、狭い帯域は誤解を招く数値になります。

python benchmarks/ceiling.py で再現できます — そのスクリプトは正確にこの表を生成し、上記の数値はその実際の出力です。タイミングはマシン依存ですが、判定と列挙数は依存しません。

明確に述べる価値のある2つの結果があります。人々が間違って推測するものだからです — そしてこのREADMEの以前のバージョンが両方間違っていたからです:

• 2変数のボックスが2^32全体に及ぶ場合でも決定されます、0.5秒未満で。このREADMEは以前、拒否されると主張していました。

• 最も広い変数を狭めても役に立ちません。 それはすでに無料です。OUT_OF_SCOPE になった場合は、他の変数の1つを狭めてください。拒否メッセージはどの変数が自由であるかを示します。

3つ以上の変数で完全な32ビットドメインを決定するには、列挙しない決定手続き — 再生可能な証明書を持つソルバーフリーの消去法 — が必要です。その手続きはこのパッケージの一部ではありません。 この層は、列挙できるボックスに対して実際の判定を提供し、できないものに対して正直な拒否を提供します。

完全なマシンワードドメインに対する判定が必要な場合、それは商用オファリングです。

ツールが回答を拒否するもの

判定は、質問が反対の結果になり得た場合にのみ価値があります。これらは回答される代わりに OUT_OF_SCOPE で拒否されます:

各拒否は問題の変数を指名し、何を変更すべきかを示します。

Pythonから使用

ツール層はトランスポート非依存なので、MCPなしで呼び出すことができます:

from crs_mcp import certify_guard

v = certify_guard(
    domain=[{"coeff": {"payload": -1}}, {"coeff": {"payload": 1}, "const": -255}],
    guard=[{"coeff": {"payload": 1, "record_len": -1}, "const": 19}],
    safety=[{"coeff": {"payload": 1, "record_len": -1}, "const": 3}],
    box={"payload": [0, 255], "record_len": [0, 255]},
)
print(v.verdict)  # CERTIFIED

アトムは、プレーンな整数（モデルが生成するもの）またはディスク上の certkit 形式の [分子, 分母] ペアのいずれかを受け入れます。

MCPでなくても? ツールはとにかく動作します

MCPはこのパッケージが構築されたトランスポートですが、ツールはJSONを受け取りJSONを返す単なる関数です。それらにはフレームワーク — またはサーバーさえ — は必要ありません:

from crs_mcp import call, openai_tools, anthropic_tools, json_schemas

call("decide_guard", {"guard": [...], "safety": [...], "box": {...}})   # run one, no server
openai_tools()       # OpenAI function-calling schema, for `tools=`
anthropic_tools()    # Anthropic tool-use schema (input_schema, not parameters)
json_schemas()       # standalone JSON Schema documents, one per tool

python -m crs_mcp.adapters anthropic > tools.json    # paste into an agent config

LangChainユーザーは crs_mcp.adapters.langchain_tools() を利用できます。LangChainはこのパッケージの依存関係ではありません。この関数は呼び出し時にそれをインポートし、欠落している場合はインストール手順とともに例外を発生させます。部分的な統合を静かに返すことはありません。

これらはすべて1つのカタログ（crs_mcp.catalog）から生成され、標準ライブラリ以外は何もインポートしません — スキーマは以前はMCPサーバーモジュール内にあり、mcp がインストールされていないと到達不能でした。

説明は重要です。 各説明は、判定が確立しないことを述べています。なぜなら OUT_OF_SCOPE を「問題なし」と読むエージェントは安全でないコードをマージするからです。名前とスキーマを保持しながらそれらの文を落としたアダプターは完全に正しく見えるでしょう。そのため check_descriptions_intact() が存在し、すべてのアダプターの出力がそれに対してテストされています。OUT_OF_SCOPE をブール値、スコア、または合格にマッピングするアダプターはありません。

サポートされているMCPバージョン

mcp 1.9.0 から 1.29.0 で検証済みで、>=1.9.0,<2.0.0 に固定されています。

mcp 2.0.0 はサーバーデコレータAPIを変更し（Server.list_tools は存在しなくなりました）、まだサポートされていません — CIは2.0.0がリリースされた日にこれを検出しました。2.xのサポートはここで主張するのではなく、将来の作業として追跡されています。

スコープ

• 線形整数算術のみ。 非線形項、ヒープ形状、エイリアシングはフラグメントの範囲外です。ツールはそうでないふりをしません。

• カウントはトリガー可能性であり、重大度ではありません。 一様サンプリング下での禁止状態の到達可能性を制限します。CVSSではなく、武器化可能性の主張でもありません。

• CERTIFIED はボックスに限定されます。 それは実ドメイン上の実証明であり、そのドメイン外のすべてについては沈黙しています。

関連

• certkit — 証明書形式と独立チェッカー

• exploit-counter — 内部の数え上げエンジン

テスト

pip install -e ".[dev]"
pytest

252件のテスト。test_tools.pyは判定（verdict）の意味論をカバーし、test_server.pyは登録されたハンドラを通して実際のtools/listとtools/callのラウンドトリップを行います。なぜなら、ツール関数は完璧でもハンドラの登録を誤っているサーバーは、もう一方のファイルのすべてのテストに合格してしまうからです。

test_adversarial.pyには最も重要なテストが含まれています。そのオラクルは単一の文です — いかなる入力も、自信ありげに見えて間違った答えを生み出してはならない — そしてCERTIFIEDを特に攻撃します。なぜなら、それはエージェントが「承認済み、コミットせよ」と読む単語だからです。また、差分テストも含んでいます：certkitとexploit-counterは同じ問いに対する独立した実装（有理数の反駁算術 vs. 整数の列挙）であり、両者はすべての入力に対して総当たりと相互検証されます。両者の不一致は、誤っている側の健全性バグです。

ドキュメント

ツールキットの残り

閉じられたコア

これらのパッケージは検査側です。意図的に証明探索を含んでいません。それが監査可能なほど小さく保つ理由であり、上流の何かが証明書を生成しなければならないことを意味します。

完全なマシンワード領域にわたる義務については、列挙はスケールせず、列挙しない決定手続きが必要です：再生可能な証明書を発行するソルバーフリーの消去法。そのエンジン、反駁から最小ガードを導出する修復合成器、そしてそれらを駆動する進化的探索は、このリポジトリには含まれておらず、商用で利用可能です。

この分割は意図的かつ恒久的です。チェッカーは無料であり、今後も無料です — 独立に検証できない証明書は無価値であり、検証に課金すればフォーマットの目的を損なうからです。お金がかかるのは、証明書を大規模に生成することです。

ライセンス

クライアントおよびツール層はApache-2.0。

高速パス数値の導出方法

上記で引用した高速化は6.06x中央値、3.55x〜10.25x観測値、形状あたり11回のペア反復です。そこに至るまでに2回間違えており、その記録はここに残されています — 数字の前にではなく、数字の下に、数字を監査したい読者が見つけられる場所に。

• 撤回 — 6.18x。 サンプルが小さすぎて、それに付随して引用された範囲を裏付けることができませんでした。

• 2026-07-31 訂正 — 2026-07-30の訂正自体が裏付けのないものでした。 2026-07-30に以前公開された数値（1,698.7 ms -> 245.7 ms、6.82x中央値（範囲6.65-6.98x）、7回のペア反復）はどのアーティファクトにも存在せず、算術も整合しません：1,698.7 / 245.7 = 6.91であり、6.82ではありません。引用された範囲も測定されたすべての形状よりも狭く — 置き換えられた6.18xの数値がすでに抱えていたのと同じnが小さすぎるエラーでした。

• 現在の数値はmake bench-fast-path（artifacts/crs/bench_fast_path.json）のコミット済み出力です：形状あたり11回のペア反復、すべての反復でビット単位で同一のカウント、そしてその部分集合ではなく実際に観測されたものから引用された範囲。

これが到達したルール：このリポジトリのパフォーマンス主張はコミット済みハーネスで再生成可能でなければならず、範囲は最良の数件ではなく測定値から来なければなりません。

ライセンス、引用、貢献

Apache-2.0（LICENSE）。これを公開する作業で使用する場合、CITATION.cffに機械可読な引用メタデータがあります — GitHubの「Cite this repository」ボタンがそれを読み取ります。

• CONTRIBUTING.md — ハウスルールと、変更が破ってはならない唯一の不変条件。

• ARCHITECTURE.md — モジュールマップと信頼境界の位置。

• TROUBLESHOOTING.md — 実際に出力されるエラーメッセージに対応。

• SECURITY.md — 偽のものを受け入れるチェッカーは、ここで最も深刻度の高いクラスです。

**certified discovery**の一部 — 1つの非対称性に基づいて構築された10のアーティファクト：証明の検査は安価で監査可能であり、したがってそれを生成したものは信頼される必要がない。