crs-mcp

Der Agent, der Ihren Patch geschrieben hat, kann seine eigenen Hausaufgaben nicht benoten.

Jetzt ausprobieren, ohne Installation: Browser-Demo öffnen und Load a forgery drücken — der Prüfer lehnt es ab, clientseitig.

Ein MCP-Server, der KI-Codierungsagenten eine Bewertungsoberfläche bietet, an der sie nicht vorbeireden können. Der Agent schlägt eine Wächterbedingung vor; dieser entscheidet, ob die Wächterbedingung tatsächlich stichhaltig ist, und liefert ein konkretes Gegenbeispiel, wenn sie es nicht ist.

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

Vorabversion. Der PyPI-Name ist reserviert und die Veröffentlichung steht unmittelbar bevor; bis dahin ist die obige Zeile die funktionierende Installation. Sie wird in CI auf Linux, macOS und Windows getestet.

30-Sekunden-Schnellstart

Fügen Sie es zu Claude Desktop (claude_desktop_config.json) oder Cursor hinzu:

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

Dann fragen Sie Ihren Agenten: "Ich habe vor diesem Lesezugriff eine Grenzprüfung 1 + payload <= record_len hinzugefügt. Zertifiziere sie gegen 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
  }
}

Das ist ein echtes Gegenbeispiel: Bei payload=0, record_len=1 besteht die Wächterbedingung und die Sicherheitseigenschaft gilt nicht. Der Agent kann nicht dagegen argumentieren, und Sie auch nicht.

Related MCP server: Chiasmus

Die drei Bewertungen

OUT_OF_SCOPE ist die wichtige. Es ist kein Fehler und es ist ausdrücklich kein Bestehen. Ein Agent wird "keine Fehler" als "genehmigt" lesen und committen; die Tool-Beschreibungen sind so geschrieben, dass sie dieser Lesart entgegenwirken, und explain_refusal liefert Prosa, die "Behandeln Sie dies nicht als Genehmigung" in so vielen Worten sagt. Ein Tool, das nur Grün zurückgibt, ist schlimmer als kein Tool.

Tools

verify_certificate gibt zusätzlich certificate_verdict zurück, das certkit's eigenes ACCEPTED / REFUSED / UNVERIFIED ist. Ein Zertifikat, das nicht besteht, wird als OUT_OF_SCOPE gemeldet, niemals als PROVEN_UNSOUND: Ein schlechter Beweis ist das Fehlen von Beweisen, nicht ein Beweis für Unzuverlässigkeit. Nur das Zählen von Zuständen kann eine Wächterbedingung als unzuverlässig beweisen, was certify_guard tut.

decide_guard: dieselbe Antwort, schneller

Meistens fragt ein Agent ist das sicher?, nicht wie unsicher?. decide_guard stoppt beim ersten entkommenden Zustand, anstatt die gesamte Region zu zählen. Gemessen an einer unzuverlässigen Wächterbedingung:

Regenerieren Sie mit python benchmarks/decide_vs_count.py im exploit-counter-Repository, wo das Zählen stattfindet. Die Lücke wächst mit der Box, weil das Zählen die gesamte verletzende Region aufzählt und das Entscheiden beim ersten entkommenden Zustand stoppt.

Identische Bewertungen — ein Test stellt sicher, dass sie bei 150 zufälligen Spezifikationen übereinstimmen. Stichhaltige Wächterbedingungen kosten in beiden Fällen gleich viel, weil die vollständige Aufzählung tatsächlich erforderlich ist, um Stichhaltigkeit festzustellen.

Das Ergebnis trägt kein over_acceptance-Feld. Es wurde nichts gezählt, daher wäre die Angabe einer Zahl dort, selbst Null, eine Zahl, die die Analyse nicht erzeugt hat.

Wie es entscheidet, und die ehrliche Grenze

Die Zertifizierung erfolgt durch erschöpfendes ganzzahliges Zählen über die von Ihnen deklarierte Box. Das ist stichhaltig und vollständig für diese Box — und sagt nichts außerhalb davon aus, weshalb die Box ein erforderliches Argument ist und nicht aus dem Kontext abgeleitet wird.

Der Zähler zählt jede Variable außer der breitesten auf, die er in geschlossener Form löst. Die Kosten sind also das Produkt der anderen Bereiche, und die Obergrenze gilt für dieses Produkt — nicht für das Boxvolumen. Die Grenze liegt bei 500.000 aufgezählten Punkten. Gemessen auf dieser Maschine:

Die Millisekundenspalte stammt von einer Maschine und wird auf Ihrer anders sein; python benchmarks/ceiling.py regeneriert diese Tabelle auf Ihrer. Die Volumina, die aufgezählten Anzahlen und die Bewertungen sind exakt und maschinenunabhängig.

Jede Entscheidung innerhalb der Grenze landet unter einer Viertelsekunde, sodass ein Agentenaufruf nicht ins Stocken gerät. Das war vorher nicht so: Die Profilierung des schlechtesten Falls zeigte ~70% der Zeit in Pythons Fraction-Typ, daher führt exploit-counter jetzt eine reine Ganzzahl-Schleife aus, wenn jeder Koeffizient eine Ganzzahl ist (was jede Grenzrelation ist). Ganzzahlen sind eine Teilmenge der rationalen Zahlen, also ist dies dieselbe Arithmetik — keine schnellere Näherung — und test_integer_and_rational_paths_agree prüft die beiden Implementierungen gegeneinander.

Auf der dichtesten Form ist das 1.491,2 ms → 244,6 ms; über alle drei gemessenen Formen ein Median von 6,06x, mit 3,55x–10,25x beobachtet. Elf gepaarte Wiederholungen pro Form, Anzahlen bitidentisch bei jeder. Regenerieren Sie mit make bench-fast-path; die Zahlen stammen aus der committeten artifacts/crs/bench_fast_path.json, nicht von dieser Seite. Zitieren Sie den Median — der Bereich bewegt sich mit Maschinenlast und Problemform, also wäre ein schmales Band die irreführende Zahl zum Wiederholen.

Reproduzieren Sie mit python benchmarks/ceiling.py — dieses Skript erzeugt genau diese Tabelle, und die obigen Zahlen sind seine echte Ausgabe. Zeitangaben sind maschinenabhängig; die Bewertungen und aufgezählten Anzahlen sind es nicht.

Zwei Konsequenzen, die es wert sind, klar ausgesprochen zu werden, weil sie die sind, die Leute falsch raten — und weil die frühere Version dieser README beide falsch hatte:

• Eine Zwei-Variablen-Box, die den gesamten 2^32-Bereich abdeckt, wird entschieden, in unter einer halben Sekunde. Diese README behauptete zuvor, sie würde abgelehnt.

• Das Verengen der breitesten Variable hilft nicht. Sie ist bereits kostenlos. Wenn Sie OUT_OF_SCOPE erhalten, verengen Sie eine der anderen; die Ablehnungsmeldung nennt, welche Variable die freie ist.

Das Entscheiden eines vollständigen 32-Bit-Bereichs in drei oder mehr Variablen erfordert ein Entscheidungsverfahren, das nicht aufzählt — eine lösungsmittelfreie Eliminationsmethode mit reproduzierbaren Zertifikaten. Dieses Verfahren ist nicht Teil dieses Pakets. Diese Stufe gibt Ihnen echte Bewertungen für die Boxen, die es aufzählen kann, und eine ehrliche Ablehnung für die, die es nicht kann.

Wenn Sie Bewertungen über vollständige Maschinenwortbereiche benötigen, ist das das kommerzielle Angebot.

Was das Tool sich weigert zu beantworten

Eine Bewertung ist nur etwas wert, wenn die Frage auch anders hätte ausgehen können. Diese werden mit OUT_OF_SCOPE abgelehnt, nicht beantwortet:

Jede Ablehnung nennt die betreffende Variable und sagt, was zu ändern ist.

Verwendung aus Python

Die Tool-Schicht ist transportunabhängig, sodass Sie sie ohne MCP aufrufen können:

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

Atome akzeptieren entweder einfache Ganzzahlen (was ein Modell produzieren wird) oder die [Zähler, Nenner]-Paare des On-Disk-certkit-Formats.

Nicht auf MCP? Die Tools funktionieren trotzdem

MCP ist der Transport, um den dieses Paket herum gebaut wurde, aber die Tools sind nur Funktionen, die JSON entgegennehmen und JSON zurückgeben. Nichts an ihnen erfordert ein Framework — oder sogar einen 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-Benutzer erhalten crs_mcp.adapters.langchain_tools(). LangChain ist keine Abhängigkeit dieses Pakets; die Funktion importiert es beim Aufruf und wirft mit einer Installationsanweisung, wenn es fehlt, anstatt stillschweigend eine partielle Integration zurückzugeben.

Alle diese werden aus einem Katalog (crs_mcp.catalog) generiert, der nichts außerhalb der Standardbibliothek importiert — die Schemata lebten früher im MCP-Servermodul und waren daher unerreichbar, es sei denn, Sie hatten mcp installiert.

Die Beschreibungen sind tragend. Jede stellt fest, was eine Bewertung nicht feststellt, weil ein Agent, der OUT_OF_SCOPE als "keine Probleme gefunden" liest, unsicheren Code zusammenführen wird. Ein Adapter, der diese Sätze fallen ließ, während er Name und Schema behielt, würde perfekt korrekt aussehen, daher existiert check_descriptions_intact() und die Ausgabe jedes Adapters wird dagegen getestet. Kein Adapter bildet OUT_OF_SCOPE auf einen booleschen Wert, eine Punktzahl oder ein Bestehen ab.

Unterstützte MCP-Versionen

Verifiziert gegen mcp 1.9.0 bis 1.29.0 und gepinnt auf >=1.9.0,<2.0.0.

mcp 2.0.0 hat die Server-Dekorator-API geändert (Server.list_tools existiert nicht mehr) und wird noch nicht unterstützt — CI hat das am Tag der Veröffentlichung von 2.0.0 erwischt. 2.x-Unterstützung wird als zukünftige Arbeit verfolgt, nicht hier beansprucht.

Umfang

• Nur lineare ganzzahlige Arithmetik. Nichtlineare Terme, Heap-Form und Aliasing sind außerhalb des Fragments. Das Tool wird nicht so tun, als wäre es anders.

• Die Zählung ist Auslösbarkeit, nicht Schweregrad. Sie begrenzt die Erreichbarkeit eines verbotenen Zustands unter gleichmäßiger Stichprobenentnahme. Sie ist kein CVSS und keine Behauptung über Waffenfähigkeit.

• CERTIFIED ist auf die Box beschränkt. Es ist ein echter Beweis über einem echten Bereich und schweigt über alles außerhalb dieses Bereichs.

Verwandt

• certkit — das Zertifikatsformat und der unabhängige Prüfer

• exploit-counter — die Zähl-Engine darunter

Tests

pip install -e ".[dev]"
pytest

252 Tests. test_tools.py deckt die Verdict-Semantik ab; test_server.py führt echte tools/list- und tools/call-Roundtrips durch die registrierten Handler aus, denn ein Server, dessen Tool-Funktionen einwandfrei sind, dessen Handler aber falsch registriert sind, würde jeden Test in der anderen Datei bestehen.

test_adversarial.py enthält diejenigen, die am wichtigsten sind. Sein Orakel ist ein einziger Satz — keine Eingabe darf eine selbstbewusst wirkende Antwort erzeugen, die falsch ist — und es greift CERTIFIED gezielt an, weil das das Wort ist, das ein Agent als „genehmigt, committe es" liest. Es trägt auch den differenziellen Test: certkit und exploit-counter sind unabhängige Implementierungen derselben Frage (rationale Widerlegungsarithmetik vs. ganzzahlige Aufzählung), und beide werden bei jeder Eingabe gegen Brute Force kreuzgeprüft. Eine Abweichung zwischen ihnen ist ein Soundness-Bug in demjenigen, der falsch liegt.

Dokumentation

Der Rest des Toolkits

Der geschlossene Kern

Diese Pakete sind die prüfende Hälfte. Sie enthalten bewusst keine Beweissuche, was sie klein genug hält, um sie zu auditieren — und es bedeutet, dass etwas vorgelagert Zertifikate erzeugen muss.

Für Verpflichtungen über vollständige Maschinenwort-Domänen skaliert Aufzählung nicht, und es ist ein Entscheidungsverfahren erforderlich, das nicht aufzählt: lösungsmittelfreie Eliminierung, die replaybare Zertifikate ausgibt. Diese Engine, der Reparatur-Synthetisierer, der aus einer Widerlegung eine minimale Absicherung ableitet, und die evolutionäre Suche, die beide antreibt, sind nicht in diesem Repository und kommerziell erhältlich.

Die Trennung ist bewusst und dauerhaft. Der Prüfer ist kostenlos und wird es immer sein — ein Zertifikat, das du nicht unabhängig verifizieren kannst, ist nichts wert, daher würde eine Gebühr für die Verifikation das Format zunichtemachen. Was Geld kostet, ist das Erzeugen von Zertifikaten in großem Maßstab.

Lizenz

Apache-2.0 für die Client- und Tool-Schicht.

Wie die Fast-Path-Zahl zustande kam

Die oben genannte Beschleunigung ist 6.06x Median, 3.55x–10.25x beobachtet, 11 gepaarte Wiederholungen pro Form. Sie kam zustande, indem sie zuerst zweimal falsch lag, und die Aufzeichnung wird hier aufbewahrt — unterhalb des Ergebnisses, wo ein Leser, der die Zahl auditieren möchte, sie finden kann, statt vor der Zahl selbst.

• Zurückgezogen — 6.18x. Die Stichprobe war zu klein, um das damit angegebene Band zu stützen.

• KORRIGIERT 2026-07-31 — die Korrektur vom 2026-07-30 war selbst nicht belegt. Die zuvor am 2026-07-30 veröffentlichten Zahlen (1.698,7 ms -> 245,7 ms, ein 6.82x Median (Spanne 6.65-6.98x), 7 gepaarte Wiederholungen) erscheinen in keinem Artefakt, und die Arithmetik geht nicht auf: 1.698,7 / 245,7 = 6.91, nicht 6.82. Das angegebene Band war außerdem schmaler als jede gemessene Form — derselbe n-zu-klein-Fehler, den die überholte 6.18x-Zahl bereits trug.

• Die aktuelle Zahl ist die festgeschriebene Ausgabe von make bench-fast-path (artifacts/crs/bench_fast_path.json): 11 gepaarte Wiederholungen pro Form, bei jeder Wiederholung bitidentische Zählungen, und eine Spanne, die aus dem tatsächlich Beobachteten zitiert wird und nicht aus einer Teilmenge davon.

Die Regel, zu der das führte: Eine Leistungsbehauptung in diesem Repository muss durch einen festgeschriebenen Harness regenerierbar sein, und die Spanne muss aus den Messungen stammen und nicht aus den besten wenigen.

Lizenz, Zitation, Mitwirkung

Apache-2.0 (LICENSE). Wenn du dies in veröffentlichter Arbeit verwendest, gibt es maschinenlesbare Zitationsmetadaten in CITATION.cff — der „Cite this repository"-Button von GitHub liest sie.

• CONTRIBUTING.md — die Hausregeln und die eine Invariante, die eine Änderung nicht brechen darf.

• ARCHITECTURE.md — die Modulkarte und wo die Vertrauensgrenze liegt.

• TROUBLESHOOTING.md — abgestimmt auf die Fehlermeldungen, die dies tatsächlich ausgibt.

• SECURITY.md — ein Prüfer, der etwas Falsches akzeptiert, ist hier die schwerwiegendste Schweregradklasse.

Teil von certified discovery — zehn Artefakte, aufgebaut auf einer Asymmetrie: Das Prüfen eines Beweises ist billig und auditierbar, also muss das, was ihn erzeugt hat, nicht vertraut werden.