minicheck-mcp

Un verificador de modelos como servidor MCP. Deja que el agente verifique la máquina de estados en lugar de adivinar.

Por qué existe esto

Los agentes diseñan máquinas de estados constantemente — bucles de reintento, protocolos de bloqueo, ciclos de vida de sesiones, traspasos entre subagentes — y luego razonan sobre la corrección en prosa. El razonamiento en prosa sobre concurrencia falla de la misma manera para un modelo que para una persona: considerando los intercalados que vienen a la mente y perdiéndose el que no viene.

Un agente con un procedimiento de decisión no tiene que adivinar. Obtiene un veredicto y, cuando la propiedad falla, la secuencia exacta de pasos que la rompe — que es también lo que necesita para corregir el diseño en lugar de disculparse por él.

La especificación que envía es datos, nunca código, por lo que nada de lo que el agente envía se ejecuta — y lo que devuelve es un veredicto con un contraejemplo más corto.

Related MCP server: agent-gate

Instalación

# 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 todavía no funciona — el paquete no está en PyPI. Instala desde GitHub como se muestra arriba; eso incluye minicheck automáticamente. python build_pypi.py produce un artefacto subible a PyPI para cuando ambos paquetes estén publicados (PyPI rechaza la referencia de dependencia directa que este paquete usa para seguir siendo instalable sin un índice).

Luego regístralo (claude_desktop_config.json, o cualquier cliente MCP):

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

El repositorio incluye esto como mcp.json.

Inicio rápido en 30 segundos

Pídele al agente: "Tengo un bucle de reintento que incrementa un contador hasta que tiene éxito. Comprueba que no puede reintentar más de 3 veces." Envía esta especificación a 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}}}
}

y obtiene de vuelta — reprodúcelo con 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"
}

No "esto podría quedarse en bucle para siempre" — los cuatro pasos exactos que lo rompen.

Lee toda la respuesta, sin embargo, y este inicio rápido es la razón: exhaustive es false. La refutación se mantiene independientemente — un contraejemplo lleva su propio testigo y ese rastro se reproduce — pero nada más en esta especificación se estableció, porque attempt no tiene guarda y lleva tries más allá de int_bound. Refutar toma un testigo; probar toma todo el espacio.

Tutorial — cómo se ve una sesión real

El agente ha escrito un ciclo de vida de sesión y quiere saber si una sesión puede usarse después de que se haya cerrado. Aquí está todo el intercambio.

1. El agente pide el formato (spec_help), luego envía 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. Obtiene una refutación con el camino exacto:

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

El invariante tal como está escrito prohíbe haber usado alguna vez una sesión cerrada, que no es lo que el agente quería decir — quería decir "ninguna transición use mientras esté cerrada". El contraejemplo hace la diferencia concreta en lugar de dejarla a un párrafo que suena plausible.

3. El agente corrige el modelo y vuelve a ejecutar. used debería significar "usado desde que esta sesión se abrió", así que close lo limpia:

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

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

PROVED y exhaustive: true es el par que hay que leer. El primero no puede emitirse sin el segundo, pero comprobar ambos hace explícito el hábito — y el hábito es lo que te protege el día que una especificación crece más allá del límite.

4. Lo que el agente no debe hacer. Si la respuesta es "verdict": "UNDETERMINED", eso no es un aprobado. Significa que la búsqueda se detuvo temprano — lee incomplete_reason y advice, acota el campo creciente, y pregunta de nuevo. Si ok es false, no existe ningún veredicto y all_hold es null.

Herramientas

El formato de especificación

{
  "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 es una conjunción de pruebas field == value (omítelo para siempre habilitado). set asigna un literal, o {"incr": n} / {"decr": n} para enteros. Un invariante es {"forbid": {...}} (falla cuando cada campo listado coincide) o {"require": {...}} (falla a menos que lo hagan).

Los enteros están acotados, y el límite se comprueba — int_bound (por defecto 64) es la magnitud más grande que un campo puede tener. Una ejecución que llevaría un campo más allá de eso se detiene y reporta exhaustive: false en lugar de saturar el valor, porque una búsqueda truncada silenciosamente reporta "se cumple" para estados que nunca visitó. Consulta Alcance honesto para saber cómo leer el veredicto resultante.

Por qué declarativo

Un servidor MCP que ejecutara Python suministrado por el agente sería un agujero de ejecución remota de código con pasos extra. Las especificaciones aquí son datos: un valor de campo que parece __import__('os').system(...) sigue siendo un string y se compara como tal. Hay una prueba que afirma exactamente eso.

¿Sin SDK? Sigue siendo utilizable.

Las herramientas son funciones simples. dispatch es el mismo punto de entrada que usa el transporte, así que puedes llamarlo desde un script o una prueba sin un agente en el bucle:

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

Sin mcp instalado, minicheck-mcp imprime un error JSON explicando cómo instalarlo y sale con código no cero, en lugar de mostrar un traceback.

Alcance honesto

Lee el veredicto como de tres valores. Esta es la parte que más importa para un agente, porque un agente lee un campo y actúa sobre él en lugar de aplicar juicio a un párrafo.

Cada respuesta también lleva verdict_means, una explicación de una línea que un agente puede citar a un usuario textualmente en lugar de parafrasearla (y posiblemente suavizarla).

Cada respuesta lleva all_hold y holds explícitamente, incluidos los errores. Una versión anterior los omitía en caso de fallo, por lo que result.get("all_hold") devolvía None tanto para un bloqueo como para un resultado genuinamente indeterminado — y ambos son falsy, exactamente como una refutación.

Cuando exhaustive es false, la respuesta también lleva incomplete_reason y advice nombrando qué cambiar. Un array warnings aparece cuando un invariante se satisface trivialmente — realmente se cumple, pero no verifica nada.

Lo que prueba. Que una máquina de estados declarativa finita satisface o no un invariante sobre cada intercalado, dentro de los límites declarados.

Lo que no prueba.

• Nada sobre tu implementación — solo sobre la especificación que enviaste. Una especificación abstrae.

• Nada fuera de int_bound (por defecto 64) o el límite de 200,000 estados. Exceder cualquiera produce UNDETERMINED, nunca un aprobado silencioso.

• Nada sobre vivacidad más allá de AG-EF, y nada en LTL.

Nada en una especificación se ejecuta jamás. Una especificación es datos: nombres de campos, literales y comparaciones. No hay eval, no hay exec, y no hay ruta de código que convierta un string en una especificación en algo invocable. Esa es la razón por la que existe el cargador declarativo en lugar de aceptar Python.

Lo que no está aquí

Este es el motor y una forma segura de llamarlo. Los corpus de propiedades de peligro mantenidos, el análisis de composición que encuentra peligros que existen solo cuando se combinan dos componentes, y el rastro de evidencia que hace que un veredicto sea auditable después son la oferta comercial. Este servidor es MIT y seguirá siéndolo.

Solución de problemas

ok: false, error: "SpecError". La especificación está mal formada y el mensaje nombra la clave. Llama validate_spec primero, o spec_help para el formato con un ejemplo trabajado.

verdict: "UNDETERMINED" en una especificación que esperaba que pasara. La búsqueda no cubrió todo el espacio de estados — usualmente un campo que crece sin límite. Lee incomplete_reason y advice. Añade una guarda when que detenga el crecimiento. No trates esto como un aprobado.

ok: false, error: "BadArguments". La herramienta fue llamada con un argumento que no acepta. Cada herramienta toma spec; check_invariant también toma un nombre de invariante opcional.

ok: false en check_liveness con "spec declares no 'goal'". La vivacidad necesita algo a lo que llegar. Añade un bloque goal con la misma forma que un invariante.

Apareció un array warnings y el invariante aún dice holds: true. El invariante nombra un valor que el espacio acotado no puede representar, por lo que se satisface por una razón no relacionada con tu protocolo — usualmente un error tipográfico en el literal, o un int_bound por debajo del valor que querías prohibir.

El servidor sale inmediatamente con un error JSON. El SDK de MCP no está instalado: pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git". Las herramientas siguen siendo importables y probables sin él mediante from minicheck_mcp import dispatch.

Mi agente trata un error como "la propiedad está bien". No debería poder hacerlo: cada respuesta lleva all_hold y holds explícitamente, y ambos son null en cualquier error, junto con verdict: "ERROR". Ramifica en result["ok"] primero.

Rendimiento

Limitado por el verificador subyacente. Las especificaciones llegan aquí declarativamente, que es la ruta compilada del verificador — aproximadamente 2.5×10⁵–7.5×10⁵ estados/segundo en CPython 3.11 en un portátil de la serie M, reproducible ejecutando python bench.py en el repositorio minicheck. Una especificación que cabe en unas pocas decenas de miles de estados responde en mucho menos de un segundo. No hay un cuello de botella medido en la capa del servidor en sí — es un despacho delgado.

FAQ

"¿No permite ejecutar código el hecho de ejecutar una especificación desde un modelo de lenguaje?" No, y por eso existe el formato declarativo. Una especificación son datos: nombres de campos, literales y comparaciones de igualdad. No hay eval, ni exec, ni ninguna ruta de código que convierta una cadena de una especificación en algo invocable. Un valor de campo que parezca __import__('os').system(...) sigue siendo una cadena y se compara como tal. Hay una prueba que afirma exactamente eso, y la suite adversarial lanza cargas con forma de código a cada herramienta. (La API Model de Python de minicheck es diferente — eso es código, y los modelos no confiables de ella merecen la misma precaución que cualquier Python no confiable. Este servidor no la expone.)

"¿Por qué no simplemente dejar que el agente escriba Python y lo ejecute?" Un servidor MCP que ejecutara Python suministrado por el agente sería un agujero de ejecución remota de código con pasos adicionales. El formato declarativo cuesta expresividad y compra una propiedad que se puede enunciar en una frase y probar.

"Mi agente leyó all_hold y concluyó que la propiedad estaba bien, pero hubo un error." No debería poder hacerlo: cada respuesta lleva all_hold y holds explícitamente, y ambos son null en cualquier error, junto con verdict: "ERROR" y ok: false. Una versión anterior omitía esos campos en caso de fallo, por lo que result.get("all_hold") devolvía None tanto para un bloqueo como para un resultado genuinamente indeterminado — y ambos son falsy, exactamente como una refutación. Primero ramifica en result["ok"], luego en verdict, nunca en la veracidad de all_hold.

"¿Por qué hay una cadena verdict_means en cada respuesta?" Porque un agente que parafrasea un veredicto tiende a suavizarlo, y "la comprobación no fue concluyente" se convierte en "parece estar bien" en dos pasos más. verdict_means es una explicación de una línea que el agente puede citar textualmente a un usuario.

"UNDETERMINED — ¿debería el agente reintentar o reportar éxito?" Ninguno por defecto. Significa que la búsqueda se detuvo temprano, por lo que no se estableció nada. Lee incomplete_reason y advice, que indican qué cambiar — normalmente un campo que crece sin límite. Acótalo y vuelve a preguntar. Reportarlo como aprobado es el modo de fallo contra el que está diseñado todo este paquete.

"¿Necesito el SDK de MCP?" Solo para servirlo a través del transporte. Las herramientas son funciones simples: from minicheck_mcp import dispatch es el mismo punto de entrada que usa el transporte, por lo que puedes llamarlo desde un script o una prueba sin un agente en el bucle. Sin mcp instalado, el comando minicheck-mcp imprime un error JSON que indica cómo instalarlo y sale con código distinto de cero, en lugar de mostrar un traceback.

"¿Está listo para producción?" Sí, y completamente probado — pero el ecosistema de agentes circundante se mueve rápido, por lo que la superficie MCP es la parte que más probablemente necesite un aumento de versión. El verificador subyacente es minicheck y es estable.

"Algo aquí me dio una respuesta segura que era incorrecta." Vale la pena abrir un issue en lugar de un workaround; por favor incluye la especificación. Un holds: true falso alcanzable desde un servidor orientado a agentes es el error más grave que puede tener este paquete, y uno de exactamente ese tipo fue encontrado, corregido y divulgado en minicheck 0.1.0.

Pruebas

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

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

102 pruebas, cada herramienta a través de la ruta real de dispatch, incluyendo entrada malformada, herramientas desconocidas y la garantía de no ejecución de código. Una de ellas afirma el propio recuento de pruebas de este README contra pytest --collect-only, por lo que la insignia no puede desviarse.

El portafolio

Una idea recorre todos ellos: un veredicto que no puedes comprobar no es un veredicto — y su corolario, que gobierna cada superficie aquí: indeterminado no es un aprobado.

Pruébalo en el navegador · verifica una máquina de estados · el leaderboard de specforge

Datos de verdad fundamental · protocol-bench · specforge

La oferta comercial

Estos son el motor. Lo que no es de código abierto es lo que lo hace útil a escala: los corpus de propiedades de peligro mantenidos, el análisis de composición que encuentra peligros que existen solo cuando se combinan dos componentes, el barrido de sensibilidad del modelo de confianza y el rastro de evidencia que hace que un veredicto sea auditable después del hecho. Las herramientas anteriores son MIT y seguirán siéndolo.

Documentación

La documentación completa, incluida la guía de conceptos y una comparación honesta contra TLA+, SPIN, Alloy y CBMC, está en https://nickharris808.github.io/verification-docs/.

Contribuciones

Los informes de errores y las solicitudes de extracción son bienvenidos — consulta CONTRIBUTING.md. Un contraejemplo que esta herramienta falle es lo más útil que puedes enviar.

Cómo citar

Los metadatos de citación están en CITATION.cff; GitHub renderiza un botón Citar este repositorio a partir de ellos.

Licencia

MIT. Consulta LICENSE.