Skip to main content
Glama

crs-mcp

ci MCP status License

El agente que escribió tu parche no puede calificar su propio trabajo.

Pruébalo ahora, sin instalación: abre la demo del navegador y pulsa Load a forgery — el verificador lo rechaza, en el lado del cliente.

Un servidor MCP que da a los agentes de codificación de IA una superficie de veredicto con la que no pueden discutir. El agente propone una guarda; esto decide si la guarda es realmente sólida y devuelve un contraejemplo concreto cuando no lo es.

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

Pre-lanzamiento. El nombre en PyPI está reservado y la publicación es inminente; hasta entonces, la línea de arriba es la instalación funcional. Está probado en CI en Linux, macOS y Windows.

Inicio rápido en 30 segundos

Añádelo a Claude Desktop (claude_desktop_config.json) o a Cursor:

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

Luego pregunta a tu agente: "He añadido una comprobación de límites 1 + payload <= record_len antes de esta lectura. Certifícala contra 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
  }
}

Eso es un contraejemplo real: en payload=0, record_len=1 la guarda pasa y la propiedad de seguridad no se cumple. El agente no puede discutirlo, y tú tampoco.

Related MCP server: Chiasmus

Los tres veredictos

Veredicto

Significado

CERTIFIED

No se admite ningún estado prohibido, en toda la caja declarada.

PROVEN_UNSOUND

Al menos uno sí — con un contraejemplo concreto.

OUT_OF_SCOPE

La caja es demasiado grande para decidirla por enumeración. No se alcanzó ningún veredicto.

OUT_OF_SCOPE es el importante. No es un fallo y, enfáticamente, no es un aprobado. Un agente leerá "sin errores" como "aprobado" y hará commit; las descripciones de las herramientas están escritas para combatir esa lectura, y explain_refusal devuelve prosa que dice "No trates esto como aprobación" en tantas palabras. Una herramienta que solo devuelve verde es peor que ninguna herramienta.

Herramientas

Herramienta

Propósito

certify_guard

¿Es esta guarda sólida sobre la caja declarada, y por cuánto?

decide_guard

El mismo veredicto, sin contar — mucho más rápido en guardas no sólidas

count_exploitability

Exactamente cuántos estados escapan, y un ejemplo

verify_certificate

Revisar un certificado certkit sin confiar en su productor

explain_refusal

Convertir un veredicto en prosa, incluyendo lo que no establece

verify_certificate además devuelve certificate_verdict, que es el propio ACCEPTED / REFUSED / UNVERIFIED de certkit. Un certificado que falla al comprobarse se reporta como OUT_OF_SCOPE, nunca como PROVEN_UNSOUND: una prueba mala es la ausencia de evidencia, no evidencia de falta de solidez. Solo contar estados puede probar que una guarda no es sólida, que es lo que hace certify_guard.

decide_guard: la misma respuesta, antes

La mayoría de las veces un agente pregunta ¿es esto seguro?, no ¿cuán inseguro?. decide_guard se detiene en el primer estado que escapa en lugar de contar toda la región. Medido en una guarda no sólida:

Caja

certify_guard (recuentos)

decide_guard (primer testigo)

Factor

payload=0:255, record_len=0:255

0.15 ms

0.0131 ms

11x

payload=0:4095, record_len=0:4095

2.29 ms

0.0134 ms

171x

payload=0:65535, record_len=0:65535

36.72 ms

0.0129 ms

2,843x

Regenera con python benchmarks/decide_vs_count.py en el repositorio exploit-counter, que es donde ocurre el conteo. La brecha crece con la caja porque contar enumera toda la región violada y decidir se detiene en el primer estado que escapa.

Veredictos idénticos — una prueba afirma que coinciden en 150 especificaciones aleatorias. Las guardas sólidas cuestan lo mismo de cualquier manera, porque la enumeración completa es realmente necesaria para establecer la solidez.

El resultado no lleva un campo over_acceptance. No se contó nada, así que reportar un número allí, incluso cero, sería una cifra que el análisis no produjo.

Cómo decide, y el límite honesto

La certificación es por conteo entero exhaustivo sobre la caja que declaras. Eso es sólido y completo para esa caja — y no dice nada fuera de ella, por eso la caja es un argumento requerido en lugar de algo inferido del contexto.

El contador enumera cada variable excepto la más amplia, que resuelve en forma cerrada. Así que el costo es el producto de los otros rangos, y el techo se aplica a ese producto — no al volumen de la caja. El límite es 500,000 puntos enumerados. Medido en esta máquina:

Caja

Volumen

Enumerados

Veredicto

Tiempo

payload=0:255, record_len=0:255

65,536

256

CERTIFIED

0 ms

payload=0:65535, record_len=0:65535

4,294,967,296

65,536

CERTIFIED

30 ms

payload=0:499999, record_len=0:10^9

5.0 × 10^14

500,000

CERTIFIED

227 ms

payload=0:500000, record_len=0:10^9

5.0 × 10^14

500,001

OUT_OF_SCOPE

0 ms

tres variables, 0:699 cada una

343,000,000

490,000

CERTIFIED

212 ms

tres variables, 0:800 cada una

513,922,401

641,601

OUT_OF_SCOPE

0 ms

La columna de milisegundos es de una máquina y diferirá en la tuya; python benchmarks/ceiling.py regenerará esta tabla en la tuya. Los volúmenes, los recuentos enumerados y los veredictos son exactos e independientes de la máquina.

Cada decisión dentro del límite cae en menos de un cuarto de segundo, así que una llamada de agente no se detiene. Eso no era cierto antes: perfilar el peor caso mostró ~70% del tiempo dentro del tipo Fraction de Python, así que exploit-counter ahora ejecuta un bucle interno solo de enteros cuando cada coeficiente es un entero (que es lo que toda relación de límites es). Los enteros son un subconjunto de los racionales, así que esta es la misma aritmética — no una aproximación más rápida — y test_integer_and_rational_paths_agree comprueba las dos implementaciones entre sí.

En la forma más densa eso es 1,491.2 ms → 244.6 ms; en las tres formas medidas, una mediana de 6.06x, con 3.55x–10.25x observado. Once repeticiones pareadas por forma, recuentos bit-idénticos en cada una. Regenera con make bench-fast-path; los números provienen del artifacts/crs/bench_fast_path.json confirmado, no de esta página. Cita la mediana — el rango se mueve con la carga de la máquina y la forma del problema, así que una banda estrecha sería el número engañoso para repetir.

Reproduce con python benchmarks/ceiling.py — ese script genera exactamente esta tabla, y los números de arriba son su salida real. Los tiempos dependen de la máquina; los veredictos y los recuentos enumerados no.

Dos consecuencias que vale la pena decir claramente, porque son las que la gente adivina mal — y porque la versión anterior de este README se equivocó en ambas:

  • Una caja de dos variables que abarca el 2^32 completo se decide, en menos de medio segundo. Este README anteriormente afirmaba que sería rechazada.

  • Reducir la variable más amplia no ayuda. Ya es gratis. Si obtienes OUT_OF_SCOPE, reduce una de las otras; el mensaje de rechazo nombra cuál variable es la libre.

Decidir un dominio completo de 32 bits en tres o más variables necesita un procedimiento de decisión que no enumere — un método de eliminación sin solvers con certificados reproducibles. Ese procedimiento no es parte de este paquete. Este nivel te da veredictos reales en las cajas que puede enumerar, y un rechazo honesto en las que no puede.

Si necesitas veredictos sobre dominios completos de palabras de máquina, esa es la oferta comercial.

Lo que la herramienta se niega a responder

Un veredicto solo vale la pena si la pregunta podría haber salido de la otra manera. Estos se rechazan con OUT_OF_SCOPE en lugar de responderse:

Entrada

Por qué se rechaza

Una caja que contiene un punto, p. ej. {"p": [0,0], "r": [0,0]}

"No se encontraron escapes" es verdad allí sin importar cuán no sólida sea la guarda.

Un rango invertido, p. ej. {"p": [10,2]}

La caja está vacía, así que un recuento de cero es vacuo.

Un átomo que nombra una variable que la caja no declara

Esa variable no está acotada; solía lanzar KeyError.

Una guarda o átomo de seguridad que falla al analizar

La entrada malformada es un rechazo con una razón, nunca un traceback.

Cada rechazo nombra la variable infractora y dice qué cambiar.

Uso desde Python

La capa de herramientas es independiente del transporte, así que puedes llamarla sin MCP en absoluto:

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

Los átomos aceptan enteros simples (lo que un modelo producirá) o los pares [numerador, denominador] del formato certkit en disco.

¿No estás en MCP? Las herramientas funcionan de todos modos

MCP es el transporte alrededor del cual se construyó este paquete, pero las herramientas son solo funciones que toman JSON y devuelven JSON. Nada sobre ellas requiere un framework — ni siquiera un servidor:

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

Los usuarios de LangChain obtienen crs_mcp.adapters.langchain_tools(). LangChain no es una dependencia de este paquete; la función lo importa al llamarse y lanza una excepción con una instrucción de instalación si falta, en lugar de devolver silenciosamente una integración parcial.

Todos estos se generan desde un catálogo (crs_mcp.catalog), que no importa nada fuera de la biblioteca estándar — los esquemas solían vivir dentro del módulo del servidor MCP y por lo tanto eran inalcanzables a menos que tuvieras mcp instalado.

Las descripciones son de carga crítica. Cada una establece lo que un veredicto no establece, porque un agente que lee OUT_OF_SCOPE como "no se encontraron problemas" fusionará código inseguro. Un adaptador que eliminara esas frases mientras mantuviera el nombre y el esquema parecería perfectamente correcto, así que check_descriptions_intact() existe y la salida de cada adaptador se prueba contra él. Ningún adaptador mapea OUT_OF_SCOPE a un booleano, una puntuación o un aprobado.

Versiones MCP compatibles

Verificado contra mcp 1.9.0 hasta 1.29.0, y fijado a >=1.9.0,<2.0.0.

mcp 2.0.0 cambió la API del decorador del servidor (Server.list_tools ya no existe) y aún no es compatible — CI lo detectó el día que se lanzó 2.0.0. El soporte 2.x se rastrea como trabajo futuro en lugar de afirmarse aquí.

Alcance

  • Solo aritmética lineal entera. Términos no lineales, forma del heap y aliasing están fuera del fragmento. La herramienta no fingirá lo contrario.

  • El recuento es de desencadenabilidad, no de severidad. Acota la alcanzabilidad de un estado prohibido bajo muestreo uniforme. No es CVSS ni una afirmación de armabilidad.

  • CERTIFIED está limitado a la caja. Es una prueba real sobre un dominio real, y es silencioso sobre todo lo que está fuera de ese dominio.

Relacionado

  • certkit — el formato de certificado y el verificador independiente

  • exploit-counter — el motor de conteo subyacente

Pruebas

pip install -e ".[dev]"
pytest

252 pruebas. test_tools.py cubre la semántica de los veredictos; test_server.py realiza tools/list y tools/call de ida y vuelta reales a través de los manejadores registrados, porque un servidor cuyas funciones de herramienta son perfectas pero cuyos manejadores están mal registrados aprobaría todas las pruebas del otro archivo.

test_adversarial.py contiene las que más importan. Su oráculo es una sola frase — ninguna entrada puede producir una respuesta de apariencia segura que sea incorrecta — y ataca a CERTIFIED de forma específica, porque esa es la palabra que un agente lee como "aprobado, consérgalo". También incluye la prueba diferencial: certkit y exploit-counter son implementaciones independientes de la misma pregunta (aritmética racional de refutación vs. enumeración de enteros), y ambas se comparan de forma cruzada contra fuerza bruta en cada entrada. Un desacuerdo entre ellas es un error de solidez en la que esté equivocada.

Documentación

SCOPE.md

qué establece cada veredicto y qué no establece

benchmarks/ceiling.py

regenera la tabla del techo de decisión anterior

TUTORIAL de certkit

ejemplo práctico completo de principio a fin

SOLUCIÓN DE PROBLEMAS de certkit

cada cadena de error del conjunto de herramientas

El resto del conjunto de herramientas

certkit

el formato de certificado y el verificador independiente

exploit-counter

si una protección no es sólida, exactamente cuántos estados escapan

crs-mcp

la superficie de veredictos a la que llaman los agentes de codificación de IA, a través de MCP

soundnessbench

el banco de pruebas que califica todo lo anterior

certkit-action

ejecuta la verificación en tu CI

pytest-mutation-verified

demuestra que tu prueba de regresión puede fallar de verdad

cve-proof-corpus

seis CVE reales con pruebas verificables por máquina

Pruébalo en tu navegador

sin instalación; observa cómo se rechaza una falsificación


El núcleo cerrado

Estos paquetes son la mitad de verificación. Contienen deliberadamente ninguna búsqueda de prueba, que es lo que los mantiene lo bastante pequeños como para auditar — y eso significa que algo anterior en la cadena tiene que producir certificados.

Para obligaciones sobre dominios completos de palabras de máquina, la enumeración no escala y se requiere un procedimiento de decisión que no enumere: eliminación sin resolvedor que emite certificados reproducibles. Ese motor, el sintetizador de reparación que deriva una protección mínima a partir de una refutación, y la búsqueda evolutiva que los impulsa no están en este repositorio y están disponibles comercialmente.

La división es deliberada y permanente. El verificador es gratuito y siempre lo será — un certificado que no puedes verificar de forma independiente no vale nada, así que cobrar por la verificación derrotaría el formato. Lo que cuesta dinero es producir certificados a escala.

Licencia

Apache-2.0 para la capa de cliente y herramientas.

Cómo se obtuvo la cifra de la ruta rápida

La aceleración citada arriba es 6.06x mediana, 3.55x–10.25x observado, 11 repeticiones emparejadas por forma. Se llegó a ella equivocándose dos veces primero, y el registro se guarda aquí — debajo del resultado, donde un lector que quiera auditar el número pueda encontrarlo, en lugar de delante del propio número.

  • Retractado — 6.18x. La muestra era demasiado pequeña para respaldar la banda citada con él.

  • CORREGIDO 2026-07-31 — la corrección del 2026-07-30 tampoco estaba respaldada. Las cifras publicadas previamente el 2026-07-30 (1,698.7 ms -> 245.7 ms, una mediana de 6.82x (rango 6.65-6.98x), 7 repeticiones emparejadas) no aparecen en ningún artefacto, y la aritmética no cuadra: 1,698.7 / 245.7 = 6.91, no 6.82. La banda citada también era más estrecha que cada forma medida — el mismo error de n demasiado pequeño que ya llevaba la cifra de 6.18x reemplazada.

  • La cifra actual es la salida confirmada de make bench-fast-path (artifacts/crs/bench_fast_path.json): 11 repeticiones emparejadas por forma, recuentos idénticos bit a bit en cada repetición, y un rango citado a partir de lo que se observó realmente en lugar de a partir de un subconjunto de ello.

La regla a la que se llegó: una afirmación de rendimiento en este repositorio tiene que poder regenerarse con un arnés confirmado, y el rango tiene que provenir de las mediciones en lugar de provenir de las mejores pocas.

Licencia, cita, contribuciones

Apache-2.0 (LICENSE). Si usas esto en un trabajo que publiques, hay metadatos de cita legibles por máquina en CITATION.cff — el botón "Cite this repository" de GitHub lo lee.

  • CONTRIBUTING.md — las reglas de la casa, y el único invariante que un cambio no debe romper.

  • ARCHITECTURE.md — el mapa de módulos y dónde se sitúa el límite de confianza.

  • TROUBLESHOOTING.md — vinculado a los mensajes de error que esto realmente imprime.

  • SECURITY.md — un verificador que acepta algo falso es la clase de gravedad más alta aquí.


Parte de descubrimiento certificado — diez artefactos construidos sobre una asimetría: verificar una prueba es barato y auditable, así que lo que la produjo no tiene que ser confiable.

Maintenance

ActivityMaintained
ResponsivenessNo issues

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

  • A
    license
    Not graded
    quality
    A
    maintenance
    MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
    79
    210
    Apache 2.0
  • A
    license
    Not graded
    quality
    B
    maintenance
    MCP server for fts-gate. It enables verification of FTS executable specifications through proof-carrying checks, exposing tools to run gate checks (fts_gate_check) and list available morphisms (fts_morphisms_list), with rejection of invalid proofs via structural logical fallacy detection.
    BSD 2-Clause "Simplified"
  • A
    license
    Not graded
    quality
    B
    maintenance
    A verification infrastructure and MCP server that specializes in refutation (negation) rather than generation, providing tools for counterexample search, Lean verification, and audit chains with a 4-value verdict system.
    MIT