minicheck-mcp

Ein Modellprüfer als MCP-Server. Lass den Agenten die Zustandsmaschine verifizieren, statt zu raten.

Warum es das gibt

Agenten entwerfen ständig Zustandsmaschinen – Wiederholungsschleifen, Sperrprotokolle, Sitzungslebenszyklen, Übergaben zwischen Unteragenten – und begründen dann die Korrektheit in Prosa. Prosa-Denken über Nebenläufigkeit scheitert bei einem Modell genauso wie bei einem Menschen: Man betrachtet die Interleavings, die einem in den Sinn kommen, und übersieht das eine, das nicht in den Sinn kommt.

Ein Agent mit einem Entscheidungsverfahren muss nicht raten. Er bekommt ein Urteil und, wenn die Eigenschaft fehlschlägt, die genaue Abfolge von Schritten, die sie bricht – was auch das ist, was er braucht, um das Design zu reparieren, statt sich dafür zu entschuldigen.

Die Spezifikation, die er sendet, ist Daten, niemals Code, also wird nichts, was der Agent einreicht, ausgeführt – und was zurückkommt, ist ein Urteil mit einer kürzesten Gegenbeispielspur.

Related MCP server: agent-gate

Installation

# 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 funktioniert noch nicht – das Paket ist nicht auf PyPI. Installiere von GitHub wie oben gezeigt; das zieht minicheck automatisch mit ein. python build_pypi.py erzeugt ein PyPI-uploadfähiges Artefakt für den Fall, dass beide Pakete veröffentlicht sind (PyPI lehnt die direkte Abhängigkeitsreferenz ab, die dieses Paket verwendet, um ohne Index installierbar zu bleiben).

Dann registriere es (claude_desktop_config.json oder ein beliebiger MCP-Client):

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

Das Repo liefert dies als mcp.json.

30-Sekunden-Schnellstart

Frag den Agenten: „Ich habe eine Wiederholungsschleife, die einen Zähler erhöht, bis sie erfolgreich ist. Prüfe, dass sie nicht mehr als 3 Mal wiederholen kann." Er sendet diese Spezifikation an 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}}}
}

und bekommt zurück – reproduzierbar mit 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"
}

Nicht „das könnte für immer schleifen" – sondern die genauen vier Schritte, die es brechen.

Lies aber die gesamte Antwort, und dieser Schnellstart ist der Grund dafür: exhaustive ist false. Die Widerlegung besteht trotzdem – ein Gegenbeispiel trägt seinen eigenen Zeugen, und diese Spur lässt sich abspielen – aber nichts anderes in dieser Spezifikation wurde bewiesen, weil attempt keine Wächterbedingung hat und tries über int_bound hinaus treibt. Widerlegen braucht einen Zeugen; Beweisen braucht den gesamten Raum.

Tutorial – wie eine Sitzung tatsächlich aussieht

Der Agent hat einen Sitzungslebenszyklus geschrieben und möchte wissen, ob eine Sitzung nach dem Schließen noch verwendet werden kann. Hier ist der gesamte Austausch.

1. Der Agent fragt nach dem Format (spec_help), dann sendet er 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. Er bekommt eine Widerlegung mit dem genauen Pfad:

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

Die Invariante, wie geschrieben, verbietet, eine geschlossene Sitzung jemals verwendet zu haben, was nicht das ist, was der Agent meinte – er meinte „kein use-Übergang, während geschlossen". Das Gegenbeispiel macht den Unterschied konkret, statt ihn in einem plausibel klingenden Absatz zu belassen.

3. Der Agent repariert das Modell und führt es erneut aus. used sollte „seit dem Öffnen dieser Sitzung verwendet" bedeuten, also löscht close es:

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

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

PROVED und exhaustive: true ist das Paar, das man lesen sollte. Das erste kann nicht ohne das zweite ausgegeben werden, aber beides zu prüfen macht die Gewohnheit explizit – und die Gewohnheit schützt dich an dem Tag, an dem eine Spezifikation über die Grenze hinauswächst.

4. Was der Agent nicht tun darf. Wenn die Antwort "verdict": "UNDETERMINED" lautet, ist das kein Bestehen. Es bedeutet, dass die Suche früh abgebrochen wurde – lies incomplete_reason und advice, begrenze das wachsende Feld und frag erneut. Wenn ok false ist, existiert überhaupt kein Urteil und all_hold ist null.

Werkzeuge

Das Spezifikationsformat

{
  "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 ist eine Konjunktion von field == value-Tests (weglassen für immer aktiv). set weist ein Literal zu, oder {"incr": n} / {"decr": n} für Ganzzahlen. Eine Invariante ist {"forbid": {...}} (schlägt fehl, wenn jedes aufgeführte Feld übereinstimmt) oder {"require": {...}} (schlägt fehl, wenn sie es nicht tun).

Ganzzahlen sind begrenzt, und die Grenze wird geprüft – int_bound (Standard 64) ist die größte Magnitude, die ein Feld halten darf. Ein Lauf, der ein Feld darüber hinaus tragen würde, stoppt und meldet exhaustive: false, statt den Wert zu sättigen, weil eine stillschweigend abgeschnittene Suche „hält" für Zustände meldet, die sie nie besucht hat. Siehe Ehrlicher Umfang für das Lesen des resultierenden Urteils.

Warum deklarativ

Ein MCP-Server, der vom Agenten geliefertes Python per exec ausführen würde, wäre ein Remote-Code-Ausführungsloch mit zusätzlichen Schritten. Spezifikationen sind hier Daten: Ein Feldwert, der wie __import__('os').system(...) aussieht, bleibt ein String und wird als solcher verglichen. Es gibt einen Test, der genau das behauptet.

Kein SDK? Trotzdem nutzbar.

Die Werkzeuge sind einfache Funktionen. dispatch ist derselbe Einstiegspunkt, den der Transport verwendet, also kannst du es aus einem Skript oder einem Test aufrufen, ohne einen Agenten in der Schleife:

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

Ohne installiertes mcp gibt minicheck-mcp einen JSON-Fehler aus, der erklärt, wie man es installiert, und beendet sich mit einem Nicht-Null-Exit-Code, statt einen Traceback zu werfen.

Ehrlicher Umfang

Lies das Urteil als dreiwertig. Das ist der Teil, der für einen Agenten am wichtigsten ist, weil ein Agent ein Feld liest und danach handelt, statt Urteilsvermögen auf einen Absatz anzuwenden.

Jede Antwort trägt auch verdict_means, eine einzeilige Erklärung, die ein Agent einem Benutzer wörtlich zitieren kann, statt sie zu paraphrasieren (und möglicherweise abzuschwächen).

Jede Antwort trägt all_hold und holds explizit, einschließlich Fehlern. Eine frühere Version ließ sie bei Fehlern weg, sodass result.get("all_hold") für einen Absturz und für ein echtes unbestimmtes Ergebnis gleichermaßen None zurückgab – und beide sind falsy, genau wie eine Widerlegung.

Wenn exhaustive false ist, trägt die Antwort auch incomplete_reason und advice, die benennen, was zu ändern ist. Ein warnings-Array erscheint, wenn eine Invariante trivial erfüllt ist – sie hält tatsächlich, verifiziert aber nichts.

Was es beweist. Dass eine endliche deklarative Zustandsmaschine eine Invariante über jede Interleaving erfüllt oder nicht, innerhalb der deklarierten Grenzen.

Was es nicht beweist.

• Nichts über deine Implementierung – nur über die Spezifikation, die du gesendet hast. Eine Spezifikation abstrahiert.

• Nichts außerhalb von int_bound (Standard 64) oder der 200.000-Zustands-Grenze. Das Überschreiten einer der beiden ergibt UNDETERMINED, niemals ein stilles Bestehen.

• Nichts über Lebendigkeit über AG-EF hinaus, und nichts in LTL.

Nichts in einer Spezifikation wird jemals ausgeführt. Eine Spezifikation ist Daten: Feldnamen, Literale und Vergleiche. Es gibt kein eval, kein exec und keinen Codepfad, der einen String in einer Spezifikation in ein aufrufbares Objekt verwandelt. Deshalb existiert der deklarative Lader, statt Python zu akzeptieren.

Was hier nicht ist

Dies ist die Engine und ein sicherer Weg, sie aufzurufen. Die gepflegten Gefahren-Eigenschafts-Korpora, die Kompositionsanalyse, die Gefahren findet, die nur existieren, wenn zwei Komponenten kombiniert werden, und die Beweiskette, die ein Urteil im Nachhinein prüfbar macht, sind das kommerzielle Angebot. Dieser Server ist MIT und bleibt es.

Fehlerbehebung

ok: false, error: "SpecError". Die Spezifikation ist fehlerhaft und die Meldung benennt den Schlüssel. Rufe zuerst validate_spec auf, oder spec_help für das Format mit einem ausgearbeiteten Beispiel.

verdict: "UNDETERMINED" bei einer Spezifikation, von der ich erwartet habe, dass sie besteht. Die Suche hat nicht den gesamten Zustandsraum abgedeckt – normalerweise ein Feld, das unbegrenzt wächst. Lies incomplete_reason und advice. Füge eine when-Wächterbedingung hinzu, die das Wachstum stoppt. Behandle dies nicht als Bestehen.

ok: false, error: "BadArguments". Das Werkzeug wurde mit einem Argument aufgerufen, das es nicht annimmt. Jedes Werkzeug nimmt spec; check_invariant nimmt zusätzlich einen optionalen invariant-Namen.

ok: false bei check_liveness mit "spec declares no 'goal'". Lebendigkeit braucht etwas, das erreicht werden kann. Füge einen goal-Block in derselben Form wie eine Invariante hinzu.

Ein warnings-Array erschien und die Invariante sagt immer noch holds: true. Die Invariante benennt einen Wert, den der begrenzte Raum nicht darstellen kann, also ist sie aus einem Grund erfüllt, der nichts mit deinem Protokoll zu tun hat – normalerweise ein Tippfehler im Literal oder ein int_bound unter dem Wert, den du verbieten wolltest.

Der Server beendet sich sofort mit einem JSON-Fehler. Das MCP-SDK ist nicht installiert: pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git". Die Werkzeuge bleiben ohne es importierbar und testbar über from minicheck_mcp import dispatch.

Mein Agent behandelt einen Fehler als „die Eigenschaft ist in Ordnung". Das sollte ihm nicht möglich sein: Jede Antwort trägt all_hold und holds explizit, und beide sind bei jedem Fehler null, zusammen mit verdict: "ERROR". Verzweige zuerst auf result["ok"].

Leistung

Begrenzt durch den zugrunde liegenden Prüfer. Spezifikationen kommen hier deklarativ an, was der kompilierte Pfad des Prüfers ist – ungefähr 2,5×10⁵–7,5×10⁵ Zustände/Sekunde in CPython 3.11 auf einem M-Series-Laptop, reproduzierbar durch Ausführen von python bench.py im minicheck-Repository. Eine Spezifikation, die in ein paar zehntausend Zustände passt, antwortet in deutlich unter einer Sekunde. Es gibt keinen gemessenen Engpass in der Server-Schicht selbst – sie ist ein dünner Dispatch.

FAQ

„Lässt das Ausführen einer Spec aus einem Sprachmodell nicht Code ausführen?" Nein, und genau dafür gibt es das deklarative Format. Eine Spec ist Daten: Feldnamen, Literale und Gleichheitsvergleiche. Es gibt kein eval, kein exec und keinen Codepfad, der eine Zeichenkette in einer Spec in einen Aufruf verwandelt. Ein Feldwert, der wie __import__('os').system(...) aussieht, bleibt eine Zeichenkette und wird als solche verglichen. Es gibt einen Test, der genau das sicherstellt, und die Adversarial-Suite feuert codeförmige Payloads auf jedes Tool. (minichecks Python-Model-API ist anders – das ist Code, und nicht vertrauenswürdige Modelle daraus verdienen dieselbe Vorsicht wie jedes nicht vertrauenswürdige Python. Dieser Server setzt sie nicht aus.)

„Warum nicht einfach den Agenten Python schreiben und ausführen lassen?" Ein MCP-Server, der vom Agenten geliefertes Python per exec ausführen würde, wäre eine Remote-Code-Execution-Lücke mit zusätzlichen Schritten. Das deklarative Format kostet Ausdruckskraft und erkauft dafür eine Eigenschaft, die man in einem Satz formulieren und testen kann.

„Mein Agent hat all_hold gelesen und daraus geschlossen, dass die Eigenschaft in Ordnung sei, aber es gab einen Fehler." Das sollte ihm nicht möglich sein: Jede Antwort enthält all_hold und holds explizit, und beide sind bei jedem Fehler null, zusammen mit verdict: "ERROR" und ok: false. Eine frühere Version hat sie bei Fehlern weggelassen, sodass result.get("all_hold") sowohl bei einem Absturz als auch bei einem echten unbestimmten Ergebnis None zurückgab – und beides ist falsy, genau wie eine Widerlegung. Prüfe zuerst result["ok"], dann verdict, niemals die Wahrheitswertigkeit von all_hold.

„Warum gibt es in jeder Antwort eine Zeichenkette verdict_means?" Weil ein Agent, der ein Urteil paraphrasiert, es tendenziell abschwächt, und aus „die Prüfung war nicht aussagekräftig" werden in zwei weiteren Schritten „sieht gut aus". verdict_means ist eine einzeilige Erklärung, die der Agent einem Benutzer wörtlich zitieren kann.

„UNDETERMINED – soll der Agent es erneut versuchen oder Erfolg melden?" Weder noch standardmäßig. Es bedeutet, dass die Suche vorzeitig abgebrochen wurde, also nichts festgestellt wurde. Lies incomplete_reason und advice, die benennen, was zu ändern ist – meistens ein Feld, das unbegrenzt wächst. Begrenze es und frage erneut. Es als bestanden zu melden, ist genau die Fehlerart, gegen die dieses gesamte Paket ausgerichtet ist.

„Brauche ich das MCP-SDK?" Nur, um es über den Transport bereitzustellen. Die Tools sind einfache Funktionen: from minicheck_mcp import dispatch ist derselbe Einstiegspunkt, den auch der Transport verwendet, sodass du es aus einem Skript oder einem Test ohne Agenten in der Schleife aufrufen kannst. Ohne installiertes mcp gibt der Befehl minicheck-mcp eine JSON-Fehlermeldung aus, die erklärt, wie man es installiert, und beendet sich mit einem Fehlercode ungleich null, statt einen Traceback zu werfen.

„Ist es produktionsreif?" Ja, und vollständig getestet – aber das umgebende Agenten-Ökosystem bewegt sich schnell, daher ist die MCP-Oberfläche der Teil, der am ehesten eine Versionserhöhung benötigt. Der darunterliegende Checker ist minicheck und ist stabil.

„Etwas hier hat mir eine selbstsichere Antwort gegeben, die falsch war." Das ist ein Issue wert, keine Problemumgehung; bitte füge die Spec bei. Ein falsches holds: true, das von einem agentenzugewandten Server erreichbar ist, ist der schwerwiegendste Fehler, den dieses Paket haben kann, und genau ein solcher wurde in minicheck 0.1.0 gefunden, behoben und offengelegt.

Tests

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

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

102 Tests, jedes Tool über den echten dispatch-Pfad, einschließlich fehlerhafter Eingaben, unbekannter Tools und der Garantie, dass kein Code ausgeführt wird. Einer davon prüft die Testanzahl dieses READMEs selbst gegen pytest --collect-only, sodass das Abzeichen nicht abweichen kann.

Das Portfolio

Eine Idee zieht sich durch alle: ein Urteil, das du nicht prüfen kannst, ist kein Urteil – und ihre Folgerung, die jede Oberfläche hier regiert: unbestimmt ist kein Bestehen.

Im Browser ausprobieren · eine Zustandsmaschine modellprüfen · das specforge-Ranglistendiagramm

Ground-Truth-Daten · protocol-bench · specforge

Das kommerzielle Angebot

Das hier ist die Engine. Was nicht Open Source ist, ist das, was sie im großen Maßstab nützlich macht: die gepflegten Gefahren-Eigenschafts-Korpora, die Kompositionsanalyse, die Gefahren findet, die nur existieren, wenn zwei Komponenten kombiniert werden, der Vertrauensmodell- Empfindlichkeitssweep und die Beweiskette, die ein Urteil im Nachhinein prüfbar macht. Die Tools oben sind MIT-lizenziert und bleiben es.

Dokumentation

Die vollständige Dokumentation, einschließlich des Konzeptleitfadens und eines ehrlichen Vergleichs mit TLA+, SPIN, Alloy und CBMC, findest du unter https://nickharris808.github.io/verification-docs/.

Mitwirken

Fehlerberichte und Pull-Requests sind willkommen – siehe CONTRIBUTING.md. Ein Gegenbeispiel, das dieses Tool falsch behandelt, ist das Nützlichste, was du senden kannst.

Zitieren

Zitationsmetadaten findest du in CITATION.cff; GitHub rendert daraus einen Cite this repository-Button.

Lizenz

MIT. Siehe LICENSE.