crs-mcp
crs-mcp
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 |
| No se admite ningún estado prohibido, en toda la caja declarada. |
| Al menos uno sí — con un contraejemplo concreto. |
| 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 |
| ¿Es esta guarda sólida sobre la caja declarada, y por cuánto? |
| El mismo veredicto, sin contar — mucho más rápido en guardas no sólidas |
| Exactamente cuántos estados escapan, y un ejemplo |
| Revisar un certificado |
| 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 |
|
| Factor |
| 0.15 ms | 0.0131 ms | 11x |
| 2.29 ms | 0.0134 ms | 171x |
| 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 |
| 65,536 | 256 | CERTIFIED | 0 ms |
| 4,294,967,296 | 65,536 | CERTIFIED | 30 ms |
| 5.0 × 10^14 | 500,000 | CERTIFIED | 227 ms |
| 5.0 × 10^14 | 500,001 |
| 0 ms |
tres variables, | 343,000,000 | 490,000 | CERTIFIED | 212 ms |
tres variables, | 513,922,401 | 641,601 |
| 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. | "No se encontraron escapes" es verdad allí sin importar cuán no sólida sea la guarda. |
Un rango invertido, p. ej. | 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 |
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) # CERTIFIEDLos á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 toolpython -m crs_mcp.adapters anthropic > tools.json # paste into an agent configLos 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.
CERTIFIEDestá 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 independienteexploit-counter— el motor de conteo subyacente
Pruebas
pip install -e ".[dev]"
pytest252 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
qué establece cada veredicto y qué no establece | |
regenera la tabla del techo de decisión anterior | |
ejemplo práctico completo de principio a fin | |
cada cadena de error del conjunto de herramientas |
El resto del conjunto de herramientas
el formato de certificado y el verificador independiente | |
si una protección no es sólida, exactamente cuántos estados escapan | |
la superficie de veredictos a la que llaman los agentes de codificación de IA, a través de MCP | |
el banco de pruebas que califica todo lo anterior | |
ejecuta la verificación en tu CI | |
demuestra que tu prueba de regresión puede fallar de verdad | |
seis CVE reales con pruebas verificables por máquina | |
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.
This server cannot be installed
Maintenance
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
MCP server providing access to the Scorecard API to evaluate and optimize LLM systems.
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
This MCP server enables users to perform scientific computations regarding linear algebra and vect…
Related MCP Servers
- AlicenseAqualityDmaintenanceMCP server that gives small LLMs verified symbolic-math & logic tools.61Apache 2.0
- AlicenseNot gradedqualityAmaintenanceMCP 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.79210Apache 2.0
- AlicenseNot gradedqualityBmaintenanceMCP 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"
- AlicenseNot gradedqualityBmaintenanceA 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