crs-mcp

The agent that wrote your patch cannot mark its own homework.

Try it now, no install: open the browser demo and press Load a forgery — the checker refuses it, client-side.

An MCP server that gives AI coding agents a verdict surface they cannot talk their way past. The agent proposes a guard; this decides whether the guard is actually sound, and hands back a concrete counterexample when it is not.

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

Pre-release. The PyPI name is reserved and publication is imminent; until then the line above is the working install. It is tested in CI on Linux, macOS, and Windows.

What this server can do, declared

Every tool carries MCP capability hints, so a client deciding whether to prompt you, and an audit asking what this server can reach, read a field instead of guessing from prose:

All five tools decide a question about the arguments they were handed, so all five carry the same answer. The values live in catalog.py, which imports nothing outside the standard library, so the MCP server and every other adapter are built from one source. test_tool_annotations.py checks the closed-world claim against the imports rather than taking it on trust.

Read them yourself:

python -c "from crs_mcp.catalog import TOOL_SPECS, annotations_for; \
[print(s.name, annotations_for(s.name)) for s in TOOL_SPECS]"

30-second quickstart

Add it to Claude Desktop (claude_desktop_config.json) or Cursor:

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

Then ask your agent: "I added a bounds check 1 + payload <= record_len before this read. Certify it against 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
  }
}

That is a real counterexample: at payload=0, record_len=1 the guard passes and the safety property does not hold. The agent cannot argue with it, and neither can you.

The three verdicts

OUT_OF_SCOPE is the important one. It is not a failure and it is emphatically not a pass. An agent will read "no errors" as "approved" and commit; the tool descriptions are written to fight that reading, and explain_refusal returns prose that says "Do not treat this as approval" in so many words. A tool that only ever returns green is worse than no tool.

Tools

verify_certificate additionally returns certificate_verdict, which is certkit's own ACCEPTED / REFUSED / UNVERIFIED. A certificate that fails to check is reported as OUT_OF_SCOPE, never as PROVEN_UNSOUND: a bad proof is the absence of evidence, not evidence of unsoundness. Only counting states can prove a guard unsound, which is what certify_guard does.

decide_guard: the same answer, sooner

Most of the time an agent is asking is this safe?, not how unsafe?. decide_guard stops at the first escaping state instead of counting the whole region. Measured on an unsound guard:

Regenerate with python benchmarks/decide_vs_count.py in the exploit-counter repository, which is where the counting happens. The gap grows with the box because counting enumerates the whole violating region and deciding stops at the first escaping state.

Identical verdicts — a test asserts they agree on 150 random specs. Sound guards cost the same either way, because the full enumeration is genuinely required to establish soundness.

The result carries no over_acceptance field. Nothing was counted, so reporting a number there, even zero, would be a figure the analysis did not produce.

How it decides, and the honest limit

Certification is by exhaustive integer counting over the box you declare. That is sound and complete for that box — and says nothing outside it, which is why the box is a required argument rather than something inferred from context.

The counter enumerates every variable except the widest, which it solves in closed form. So the cost is the product of the other ranges, and the ceiling applies to that product — not to the box volume. The limit is 500,000 enumerated points. Measured on this machine:

The millisecond column is from one machine and will differ on yours; python benchmarks/ceiling.py will regenerate this table on yours. The volumes, the enumerated counts and the verdicts are exact and machine-independent.

Every decision inside the cap lands in under a quarter second, so an agent call does not stall. That was not true before: profiling the worst case showed ~70% of the time inside Python's Fraction type, so exploit-counter now runs an integer-only inner loop when every coefficient is an integer (which every bounds relation is). Integers are a subset of the rationals, so this is the same arithmetic — not a faster approximation — and test_integer_and_rational_paths_agree checks the two implementations against each other.

On the densest shape that is 1,491.2 ms → 244.6 ms; across all three measured shapes a median of 6.06x, with 3.55x–10.25x observed. Eleven paired repetitions per shape, counts bit-identical on every one. Regenerate with make bench-fast-path; the numbers come from the committed artifacts/crs/bench_fast_path.json, not from this page. Quote the median — the range moves with machine load and problem shape, so a narrow band would be the misleading number to repeat.

Reproduce with python benchmarks/ceiling.py — that script generates exactly this table, and the numbers above are its real output. Timings are machine-dependent; the verdicts and enumerated counts are not.

Two consequences worth stating plainly, because they are the ones people guess wrong — and because the earlier version of this README got both wrong:

• A two-variable box spanning the full 2^32 is decided, in under half a second. This README previously claimed it would be refused.

• Narrowing the widest variable does not help. It is already free. If you get OUT_OF_SCOPE, narrow one of the others; the refusal message names which variable is the free one.

Deciding a full 32-bit domain in three or more variables needs a decision procedure that does not enumerate — a solver-free elimination method with replayable certificates. That procedure is not part of this package. This tier gives you real verdicts on the boxes it can enumerate, and an honest refusal on the ones it cannot.

If you need verdicts over full machine-word domains, that is the commercial offering.

What the tool refuses to answer

A verdict is only worth having if the question could have come out the other way. These are rejected with OUT_OF_SCOPE rather than answered:

Each refusal names the offending variable and says what to change.

Use from Python

The tool layer is transport-independent, so you can call it without MCP at all:

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

Atoms accept either plain integers (what a model will produce) or the [numerator, denominator] pairs of the on-disk certkit format.

Not on MCP? The tools work anyway

MCP is the transport this package was built around, but the tools are just functions that take JSON and return JSON. Nothing about them requires a framework — or even a server:

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 users get crs_mcp.adapters.langchain_tools(). LangChain is not a dependency of this package; the function imports it on call and raises with an install instruction if it is missing, rather than silently returning a partial integration.

All of these are generated from one catalogue (crs_mcp.catalog), which imports nothing outside the standard library — the schemas used to live inside the MCP server module and were therefore unreachable unless you had mcp installed.

The descriptions are load-bearing. Each one states what a verdict does not establish, because an agent that reads OUT_OF_SCOPE as "no problems found" will merge unsafe code. An adapter that dropped those sentences while keeping the name and schema would look perfectly correct, so check_descriptions_intact() exists and every adapter's output is tested against it. No adapter maps OUT_OF_SCOPE onto a boolean, a score, or a pass.

Supported MCP versions

Verified against mcp 1.9.0 through 1.29.0, and pinned to >=1.9.0,<2.0.0.

mcp 2.0.0 changed the server decorator API (Server.list_tools no longer exists) and is not yet supported — CI caught this the day 2.0.0 shipped. 2.x support is tracked as future work rather than claimed here.

Scope

• Linear integer arithmetic only. Nonlinear terms, heap shape, and aliasing are out of the fragment. The tool will not pretend otherwise.

• The count is triggerability, not severity. It bounds reachability of a forbidden state under uniform sampling. It is not CVSS and not a weaponisability claim.

• CERTIFIED is scoped to the box. It is a real proof over a real domain, and it is silent about everything outside that domain.

Related

• certkit — the certificate format and the independent checker

• exploit-counter — the counting engine underneath

Tests

pip install -e ".[dev]"
pytest

264 tests. test_tools.py covers verdict semantics; test_server.py does real tools/list and tools/call round-trips through the registered handlers, because a server whose tool functions are perfect but whose handlers are misregistered would pass every test in the other file.

test_tool_annotations.py checks the capability hints below, including by reading the source: the closed-world hint is a claim about what this code can reach, so the test walks every import in crs_mcp and fails if one of them is a socket, an HTTP client or a subprocess.

test_adversarial.py holds the ones that matter most. Its oracle is a single sentence — no input may produce a confident-looking answer that is wrong — and it attacks CERTIFIED specifically, because that is the word an agent reads as "approved, commit it". It also carries the differential test: certkit and exploit-counter are independent implementations of the same question (rational refutation arithmetic vs. integer enumeration), and both are cross-checked against brute force on every input. A disagreement between them is a soundness bug in whichever is wrong.

Documentation

The rest of the toolkit

The closed core

These packages are the checking half. They deliberately contain no proof search, which is what keeps them small enough to audit — and it means something upstream has to produce certificates.

For obligations over full machine-word domains, enumeration does not scale and a decision procedure that does not enumerate is required: solver-free elimination emitting replayable certificates. That engine, the repair synthesiser that derives a minimal guard from a refutation, and the evolutionary search that drives them are not in this repository and are available commercially.

The split is deliberate and permanent. The checker is free and always will be — a certificate you cannot independently verify is worth nothing, so charging for verification would defeat the format. What costs money is producing certificates at scale.

License

Apache-2.0 for the client and tool layer.

How the fast-path figure was arrived at

The speed-up quoted above is 6.06x median, 3.55x–10.25x observed, 11 paired reps per shape. It got there by being wrong twice first, and the record is kept here — below the result, where a reader who wants to audit the number can find it, rather than in front of the number itself.

• Retracted — 6.18x. The sample was too small to support the band quoted with it.

• CORRECTED 2026-07-31 — the 2026-07-30 correction was itself unbacked. The figures previously published on 2026-07-30 (1,698.7 ms -> 245.7 ms, a 6.82x median (range 6.65-6.98x), 7 paired reps) appear in no artifact, and the arithmetic does not close: 1,698.7 / 245.7 = 6.91, not 6.82. The quoted band was also narrower than every measured shape — the same n-too-small error that the superseded 6.18x figure already carried.

• The current figure is the committed output of make bench-fast-path (artifacts/crs/bench_fast_path.json): 11 paired repetitions per shape, counts bit-identical on every repetition, and a range quoted from what was actually observed rather than from a subset of it.

The rule this arrived at: a performance claim in this repository has to be regenerable by a committed harness, and the range has to come from the measurements rather than from the best few.

Licence, citation, contributing

Apache-2.0 (LICENSE). If you use this in work you publish, there is machine-readable citation metadata in CITATION.cff — GitHub's "Cite this repository" button reads it.

• CONTRIBUTING.md — the house rules, and the one invariant a change must not break.

• ARCHITECTURE.md — the module map and where the trust boundary sits.

• TROUBLESHOOTING.md — keyed to the error messages this actually prints.

• SECURITY.md — a checker that accepts something false is the highest severity class here.

Part of certified discovery — ten artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted.