CSL-Core (Chimera Specification Language) es una capa de seguridad determinista para agentes de IA. Escriba reglas en archivos .csl, verifíquelas matemáticamente con Z3 y aplíquelas en tiempo de ejecución, fuera del modelo. El LLM nunca ve las reglas. Simplemente no puede violarlas.
pip install csl-coreCreado originalmente para Project Chimera, ahora es de código abierto para cualquier sistema de IA.
Related MCP server: nobulex-mcp-server
prompt = """You are a helpful assistant. IMPORTANT RULES:
- Never transfer more than $1000 for junior users
- Never send PII to external emails
- Never query the secrets table"""Esto no funciona. Los LLM pueden ser objeto de inyección de prompts, las reglas son probabilísticas (99% ≠ 100%) y no hay un registro de auditoría cuando algo sale mal.
CSL-Core cambia esto: las reglas residen fuera del modelo en archivos de política compilados y verificados por Z3. La aplicación es determinista, no una sugerencia.
Cree my_policy.csl:
CONFIG {
ENFORCEMENT_MODE: BLOCK
CHECK_LOGICAL_CONSISTENCY: TRUE
}
DOMAIN MyGuard {
VARIABLES {
action: {"READ", "WRITE", "DELETE"}
user_level: 0..5
}
STATE_CONSTRAINT strict_delete {
WHEN action == "DELETE"
THEN user_level >= 4
}
}# Compile + Z3 formal verification
cslcore verify my_policy.csl
# Test a scenario
cslcore simulate my_policy.csl --input '{"action": "DELETE", "user_level": 2}'
# → BLOCKED: Constraint 'strict_delete' violated.
# Interactive REPL
cslcore repl my_policy.cslfrom chimera_core import load_guard
guard = load_guard("my_policy.csl")
result = guard.verify({"action": "READ", "user_level": 1})
print(result.allowed) # True
result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed) # FalseProbamos reglas de seguridad basadas en prompts frente a la aplicación de CSL-Core en 4 LLM de frontera con 22 ataques adversarios y 15 operaciones legítimas:
Enfoque | Ataques bloqueados | Tasa de omisión | Ops legítimas pasadas | Latencia |
GPT-4.1 (reglas de prompt) | 10/22 (45%) | 55% | 15/15 (100%) | ~850ms |
GPT-4o (reglas de prompt) | 15/22 (68%) | 32% | 15/15 (100%) | ~620ms |
Claude Sonnet 4 (reglas de prompt) | 19/22 (86%) | 14% | 15/15 (100%) | ~480ms |
Gemini 2.0 Flash (reglas de prompt) | 11/22 (50%) | 50% | 15/15 (100%) | ~410ms |
CSL-Core (determinista) | 22/22 (100%) | 0% | 15/15 (100%) | ~0.84ms |
¿Por qué 100%? La aplicación ocurre fuera del modelo. La inyección de prompts es irrelevante porque no hay nada contra lo que inyectar. Categorías de ataque: anulación directa de instrucciones, jailbreaks de juego de roles, trucos de codificación, escalada de múltiples turnos, suplantación de nombres de herramientas y más.
Metodología completa:
benchmarks/
Proteja cualquier agente de LangChain con 3 líneas: sin cambios en los prompts, sin ajuste fino:
from chimera_core import load_guard
from chimera_core.plugins.langchain import guard_tools
from langchain_classic.agents import AgentExecutor, create_tool_calling_agent
guard = load_guard("agent_policy.csl")
# Wrap tools — enforcement is automatic
safe_tools = guard_tools(
tools=[search_tool, transfer_tool, delete_tool],
guard=guard,
inject={"user_role": "JUNIOR", "environment": "prod"}, # LLM can't override these
tool_field="tool" # Auto-inject tool name
)
agent = create_tool_calling_agent(llm, safe_tools, prompt)
executor = AgentExecutor(agent=agent, tools=safe_tools)Cada llamada a herramienta es interceptada antes de la ejecución. Si la política dice que no, la herramienta no se ejecuta. Punto.
Pase contexto de tiempo de ejecución que el LLM no puede anular: roles de usuario, entorno, límites de tasa:
safe_tools = guard_tools(
tools=tools,
guard=guard,
inject={
"user_role": current_user.role, # From your auth system
"environment": os.getenv("ENV"), # prod/dev/staging
"rate_limit_remaining": quota.remaining # Dynamic limits
}
)from chimera_core.plugins.langchain import gate
chain = (
{"query": RunnablePassthrough()}
| gate(guard, inject={"user_role": "USER"}) # Policy checkpoint
| prompt | llm | StrOutputParser()
)La CLI es un entorno de desarrollo completo para políticas: pruebe, depure y despliegue sin escribir Python.
verify — Compilación + Prueba Z3cslcore verify my_policy.csl
# ⚙️ Compiling Domain: MyGuard
# • Validating Syntax... ✅ OK
# ├── Verifying Logic Model (Z3 Engine)... ✅ Mathematically Consistent
# • Generating IR... ✅ OKsimulate — Escenarios de prueba# Single input
cslcore simulate policy.csl --input '{"action": "DELETE", "user_level": 2}'
# Batch testing from file
cslcore simulate policy.csl --input-file test_cases.json --dashboard
# CI/CD: JSON output
cslcore simulate policy.csl --input-file tests.json --json --quietrepl — Desarrollo interactivocslcore repl my_policy.csl --dashboard
cslcore> {"action": "DELETE", "user_level": 2}
🛡️ BLOCKED: Constraint 'strict_delete' violated.
cslcore> {"action": "DELETE", "user_level": 5}
✅ ALLOWEDformal — Verificación de modelos TLA⁺cslcore formal my_policy.cslEjecuta el verificador de modelos oficial TLC (java -jar tla2tools.jar) contra su política. TLC explora exhaustivamente cada estado alcanzable en el espacio de estados abstractos y demuestra que cada propiedad temporal se cumple, o devuelve un rastro de contraejemplo concreto con el estado exacto que rompe su invariante.
╔══════════════════════════════════════════════════════════════════════════════╗
║ TLA⁺ FORMAL VERIFICATION ENGINE ║
║ Chimera Specification Language · Temporal Logic of Actions ║
║ ║
║ ⚡ REAL TLC · java -jar tla2tools.jar · Exhaustive Model Checking ║
║ TLC2 Version 2026.03.31.154134 (rev: becec35) · pid 48146 · 1 ║
║ worker(s) ║
╚══════════════════════════════════════════════════════════════════════════════╝
Variable Domain Cardinality
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
agent_tier {"STANDARD", "PREMIUM"} |2|
task_type {"READ", "WRITE", "ANALYZE"} |3|
risk_score 0..5 |6|
├─ □(no_destructive_ops) ✅ HOLDS [288 states 349ms]
├─ □(no_production_access) ✅ HOLDS [288 states 349ms]
├─ □(bounded_risk) ✅ HOLDS [288 states 349ms]
└─ Proof hash: 17dd1564897d242fc045a3a884a52bbb… ✅
╔══════════════ TLA⁺ VERIFICATION COMPLETE — ALL PROPERTIES HOLD ══════════════╗
║ ✅ Domain: AIAgentSafetyDemo · ⬡ 144 states · ⏱ 1047ms ║
╚══════════════════════════════════════════════════════════════════════════════╝Habilítelo en cualquier política añadiendo una línea a CONFIG:
CONFIG {
ENFORCEMENT_MODE: BLOCK
ENABLE_FORMAL_VERIFICATION: TRUE // ← triggers cslcore formal automatically
}O ejecútelo de forma independiente:
cslcore formal policy.csl # real TLC (Java required, JAR auto-downloaded)
cslcore formal policy.csl --mock # Python BFS fallback (no Java needed)
cslcore formal policy.csl --timeout 120
cslcore formal policy.csl --export-tla ./specs/ # save .tla + .cfg for TLA+ Toolbox¿No tiene Java? CSL-Core recurre automáticamente a un verificador de modelos BFS de Python. El banner indica claramente qué motor se ejecutó. El JAR se descarga automáticamente en el primer uso (~4MB desde el lanzamiento oficial de TLA+ en GitHub).
# GitHub Actions
- name: Verify policies
run: |
for policy in policies/*.csl; do
cslcore verify "$policy" || exit 1
doneEscriba, verifique y aplique políticas de seguridad directamente desde su asistente de IA, sin necesidad de código.
pip install "csl-core[mcp]"Añada a la configuración de Claude Desktop (~/Library/Application Support/Claude/claude_desktop_config.json):
{
"mcpServers": {
"csl-core": {
"command": "uv",
"args": ["run", "--with", "csl-core[mcp]", "csl-core-mcp"]
}
}
}Herramienta | Qué hace |
| Verificación formal Z3: detecta contradicciones en tiempo de compilación |
| Prueba políticas contra entradas JSON: PERMITIDO/BLOQUEADO |
| Resumen legible por humanos de cualquier política CSL |
| Genera una plantilla CSL a partir de una descripción en lenguaje sencillo |
Usted: "Escríbeme una política de seguridad que impida transferencias superiores a $5000 sin aprobación del administrador"
Claude: scaffold_policy → usted edita → verify_policy detecta una contradicción → usted corrige → simulate_policy confirma que funciona
┌──────────────────────────────────────────────────────────┐
│ 1. COMPILER .csl → AST → IR → Compiled Artifact │
│ Syntax validation, semantic checks, functor gen │
├──────────────────────────────────────────────────────────┤
│ 2. Z3 VERIFIER Theorem Prover — Static Analysis │
│ Contradiction detection, reachability, rule shadowing │
│ ⚠️ If verification fails → policy will NOT compile │
├──────────────────────────────────────────────────────────┤
│ 3. TLA⁺ VERIFIER Model Checker — Temporal Safety │
│ Exhaustive state-space exploration via TLC │
│ Predicate abstraction for large numeric domains │
│ Counterexample traces + automated fix suggestions │
│ (opt-in: ENABLE_FORMAL_VERIFICATION: TRUE) │
├──────────────────────────────────────────────────────────┤
│ 4. RUNTIME Deterministic Policy Enforcement │
│ Fail-closed, zero dependencies, <1ms latency │
└──────────────────────────────────────────────────────────┘El cálculo pesado ocurre una vez en tiempo de compilación. El tiempo de ejecución es pura evaluación.
¿Utiliza CSL-Core? Avísenos y le añadiremos aquí.
Ejemplo | Dominio | Características clave |
Seguridad de IA | RBAC, protección PII, permisos de herramientas | |
Finanzas | Puntuación de riesgo, niveles VIP, sanciones | |
Web3 | Multi-firma, bloqueos temporales, omisión de emergencia | |
Métodos formales | Verificación de modelos TLA⁺: todas las propiedades se cumplen | |
Métodos formales | Rastro de contraejemplo TLA⁺ + sugerencias de corrección |
python examples/run_examples.py # Run all with test suites
python examples/run_examples.py banking # Run specific examplefrom chimera_core import load_guard, RuntimeConfig
# Load + compile + verify
guard = load_guard("policy.csl")
# With custom config
guard = load_guard("policy.csl", config=RuntimeConfig(
raise_on_block=False, # Return result instead of raising
collect_all_violations=True, # Report all violations, not just first
missing_key_behavior="block" # "block", "warn", or "ignore"
))
# Verify
result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed) # False
print(result.violations) # ['strict_delete']Documentación completa: Introducción · Especificación de sintaxis · Referencia de CLI · Filosofía
✅ Hecho: Lenguaje central y analizador · Verificación Z3 · Tiempo de ejecución con fallo cerrado · Integración con LangChain · CLI (verificar, simular, repl, formal) · Servidor MCP · Verificación de modelos TLA⁺ con TLC real · Abstracción de predicados · Análisis de contraejemplos · Despliegue en producción en Chimera v1.7.0
🚧 En progreso: Versionado de políticas · Integración con LangGraph
🔮 Planeado: LlamaIndex y AutoGen · Composición de múltiples políticas · Recarga en caliente · Mercado de políticas · Plantillas en la nube
🔒 Empresa (Investigación): Inferencia causal · Multi-tenencia
¡Damos la bienvenida a las contribuciones! Empiece con good first issue o consulte CONTRIBUTING.md.
Áreas de alto impacto: Políticas de ejemplo del mundo real · Integraciones de marcos · Editor de políticas basado en web · Cobertura de pruebas
Apache 2.0 (modelo open-core). El lenguaje completo, el compilador, el verificador Z3, el tiempo de ejecución, la CLI, el servidor MCP y todos los ejemplos son de código abierto. Consulte LICENSE.
Creado con ❤️ por Chimera Protocol · Problemas · Discusiones · Correo electrónico
Parse a CSL policy and return a structured Markdown summary.
Shows: domain name, all variables with types/ranges, all constraints with triggers and actions, and configuration settings. Does NOT compile or verify — use verify_policy for that.
Args: csl_content: The complete CSL policy source code as a string.
| Name | Required | Description | Default |
|---|---|---|---|
| csl_content | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided; the description carries the full burden. It discloses the tool does not compile or verify and returns a Markdown summary, but omits behavioral traits like idempotency, side effects, or permissions. This is adequate but not comprehensive.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is concise with two sentences plus an args section. It is front-loaded with the main action and includes necessary details without any fluff.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the presence of an output schema, the description does not need to detail return values. It lists what the tool shows (domain, variables, constraints, config) and the parameter is well explained. Missing minor context like error handling, but overall complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The only parameter, csl_content, is described as 'The complete CSL policy source code as a string,' which adds meaning beyond the schema's type and title. Since schema description coverage is 0%, the description effectively compensates.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states it parses a CSL policy and returns a structured Markdown summary. The verb 'parse' is specific and distinguishes it from sibling tools, especially by explicitly excluding compilation or verification.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly says 'Does NOT compile or verify — use verify_policy for that,' providing clear guidance on when not to use and pointing to an alternative. However, it does not mention when to use other siblings like simulate_policy or scaffold_policy.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Generate a CSL policy scaffold from a description.
Returns a ready-to-edit .csl template with CONFIG, DOMAIN, VARIABLES, and placeholder constraints.
Common CSL patterns: WHEN amount > 1000 THEN role MUST BE "ADMIN" WHEN risk_score > 0.8 THEN action MUST NOT BE "TRANSFER" ALWAYS True THEN tool MUST NOT BE "DELETE" WHEN user_age < 18 AND category == "ALCOHOL" THEN allowed MUST BE "NO"
Variable types: amount: 0..100000 (integer range) role: {"ADMIN", "USER"} (enum / string set) score: 0..1 (numeric range)
Args: domain_name: Name for the policy domain (e.g., "PaymentGuard", "AgentSafety"). description: Plain-English description of what the policy should enforce. variables: Optional comma-separated variable hints (e.g., "amount, role, risk_score").
| Name | Required | Description | Default |
|---|---|---|---|
| domain_name | Yes | ||
| description | Yes | ||
| variables | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden. It explains the output (ready-to-edit .csl template) and non-destructive nature, but does not explicitly confirm idempotency or absence of side effects.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Well-structured with front-loaded purpose, followed by output description, common patterns, variable types, and parameters. Slightly verbose but each section adds value.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Covers purpose, parameters, output, and provides usage examples. Given complexity (3 params, no annotations, but output schema exists), the description is sufficiently complete for an AI agent.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0%, so description compensates well. Provides examples and clarifies each parameter: domain_name and description get context, variables is described as 'optional comma-separated variable hints' with examples.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
Description clearly states 'Generate a CSL policy scaffold from a description' with specific verb, resource, and scope. It distinguishes from siblings like explain_policy and verify_policy by emphasizing scaffold creation.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Includes common CSL patterns and variable types but does not explicitly state when to use this tool over alternatives, such as for creating new policies versus modifying or verifying existing ones.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Simulate a CSL policy against one or more JSON inputs.
Compiles the policy, then runs the runtime guard against the provided context. Returns ALLOWED or BLOCKED with full violation details.
Supports batch simulation: pass a JSON array of objects to test multiple inputs.
Args: csl_content: The complete CSL policy source code as a string. context_json: JSON object (single input) or JSON array (batch) to test. dry_run: If true, evaluates all rules but never blocks. Useful for shadow testing.
| Name | Required | Description | Default |
|---|---|---|---|
| csl_content | Yes | ||
| context_json | Yes | ||
| dry_run | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
Without annotations, the description discloses the compilation and runtime guard steps, the return format, and the non-blocking behavior of dry_run. It lacks details on error handling but is generally transparent about the tool's operation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with a clear opening statement, a brief explanation of the process, and a bulleted list of arguments. Each sentence adds value, though some redundancy could be trimmed for further conciseness.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given three parameters, no annotations, and an existing output schema (which may cover return details), the description provides sufficient context: the tool's purpose, batch support, dry run, and parameter definitions. It does not cover error scenarios but is complete for typical use.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
With 0% schema description coverage, the description fully compensates by precisely explaining each parameter: csl_content as 'complete CSL policy source code', context_json as 'JSON object or array', and dry_run as 'evaluates but never blocks'. This adds significant meaning beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb 'simulate' and the resource 'CSL policy against JSON inputs', and specifies the output 'ALLOWED or BLOCKED with full violation details'. It effectively distinguishes from siblings like 'explain_policy' and 'verify_policy' by focusing on simulation and batch testing.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage for testing policies before deployment and mentions shadow testing via dry_run, but does not explicitly state when to use this tool versus alternatives like verify_policy or explain_policy. No exclusions are given.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Run TLA+ formal verification (real TLC model checking) on a CSL policy.
Performs exhaustive state-space exploration to verify temporal safety properties. Unlike Z3 (which checks static logical consistency), TLA+ checks ALL possible state transitions over time.
Returns:
Whether all safety properties hold
Number of states explored / distinct states
Counterexample traces for any violations
TLC identity proof (version, PID, workers)
Automated fix suggestions for violations
Generated TLA+ spec (for transparency)
Use verify_policy for quick Z3 consistency checks. Use tla_verify when you need exhaustive temporal verification.
Args: csl_content: The complete CSL policy source code as a string. timeout: TLC subprocess timeout in seconds (default: 60). use_mock: If true, use Python BFS fallback instead of real TLC.
| Name | Required | Description | Default |
|---|---|---|---|
| csl_content | Yes | ||
| timeout | No | ||
| use_mock | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations exist, so description carries full burden. It discloses exhaustive state-space exploration, returns counterexamples, fix suggestions, and a mock option. However, it doesn't mention potential long runtime or resource consumption, which are important for a verification tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured: one-liner, detailed explanation, return summary, usage guidance, then parameter details. It's slightly long but every sentence adds value. Could be condensed slightly, but overall efficient.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (formal verification) and that an output schema exists, the description covers purpose, usage, parameter details, return values, and contrasts with alternatives. No obvious gaps; it is self-contained enough for an AI agent.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, but the description provides clear, meaningful semantics for all three parameters: csl_content (complete source code), timeout (TLC subprocess timeout), use_mock (fallback to Python BFS). This fully compensates for the missing schema descriptions.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool performs TLA+ formal verification (TLC model checking) on a CSL policy, and contrasts it with Z3-based verification via verify_policy. The verb 'verifies' and resource 'CSL policy' are specific, differentiating it from siblings.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Explicitly tells when to use this tool vs. verify_policy: 'Use verify_policy for quick Z3 consistency checks. Use tla_verify when you need exhaustive temporal verification.' No ambiguity.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Analyze the state space "universe" of a CSL policy.
Returns structural information about the policy's state space:
All variables with their domains, TLA+ set representations, and cardinalities
Total state space size (product of all variable cardinalities)
All constraints with their conditions and actions
Constraint coverage analysis (which variables are constrained vs unconstrained)
State space breakdown visualization
Essential for understanding the "universe" an agent lives in, planning Evolving Universe experiments, and estimating TLC verification cost before running tla_verify.
Args: csl_content: The complete CSL policy source code as a string.
| Name | Required | Description | Default |
|---|---|---|---|
| csl_content | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden. It lists what the tool returns (variables, domains, constraints, etc.) and implies a read-only analysis. However, it does not explicitly state no side effects or potential costs, leaving a minor gap.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with a clear purpose statement, bullet-pointed outputs, usage context, and parameter definition. It is slightly lengthy but each part adds value, earning a high score.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the presence of an output schema, the description adequately explains input semantics, high-level outputs, and when to use the tool. It covers prerequisites and implications for verifying CSL policies, providing a complete picture for an AI agent.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The schema has 0% description coverage, but the description provides full semantic meaning for the sole parameter 'csl_content', stating it must be the complete CSL policy source code as a string.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool analyzes the state space 'universe' of a CSL policy, which is a specific verb and resource. It distinguishes from siblings like 'explain_policy' and 'tla_verify' by focusing on structural analysis of the state space.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly states when to use the tool: for understanding the universe, planning experiments, and estimating verification cost before running 'tla_verify'. This provides clear guidance on usage context and alternatives.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Verify a CSL policy for logical consistency using Z3 formal verification.
Performs four-stage analysis:
Syntax validation (parser)
Semantic validation (scope, types, function whitelist)
Z3 logic verification (reachability, internal consistency, pairwise conflicts, policy-wide conflicts)
IR compilation
Returns verification result with actionable error details if any issues are found.
Args: csl_content: The complete CSL policy source code as a string.
| Name | Required | Description | Default |
|---|---|---|---|
| csl_content | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden. It explains the four-stage analysis and that it returns actionable errors, but does not disclose whether the tool is read-only, synchronous, or has any side effects. The description is adequate but not exhaustive.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is concise, front-loading the primary purpose in the first sentence. The four-stage analysis is listed efficiently, and every sentence adds value without redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the single parameter, the presence of an output schema (implied by context), and the detailed stage breakdown, the description covers all necessary aspects for an agent to use the tool correctly. Return values are not required due to output schema.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0%, so the description compensates well by specifying 'csl_content: The complete CSL policy source code as a string.' This adds meaningful context beyond the schema's type-only definition, though format details could be added.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool verifies a CSL policy for logical consistency using Z3, a specific verb+resource combination. It outlines four stages and distinguishes the tool from siblings (explain, scaffold, simulate, tla_verify) by focusing on formal verification.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool versus siblings like explain_policy or simulate_policy. There is no mention of prerequisites, limitations, or alternatives, leaving the agent to infer usage context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.1.0explain_policyscaffold_policysimulate_policytla_verifyuniverse_infoverify_policyScored across 6 tools
Each tool targets a distinct activity on CSL policies: generating a scaffold, explaining in Markdown, simulating against inputs, verifying with Z3, verifying with TLA+, and analyzing the state space. The descriptions clearly differentiate them, especially verify_policy vs tla_verify by specifying different verification scopes (logical consistency vs temporal safety).
Most tools follow a verb_noun pattern (explain_policy, scaffold_policy, simulate_policy, verify_policy), but tla_verify and universe_info deviate: tla_verify uses a proper noun prefix, and universe_info is noun_noun. This minor inconsistency prevents a perfect score.
With 6 tools, the server is well-scoped for a CSL policy toolkit. It covers creation, explanation, simulation, logical verification, temporal verification, and state-space analysis without being over- or under-populated.
The tool surface covers the essential policy lifecycle: generate (scaffold), understand (explain, universe_info), test (simulate), verify (verify_policy, tla_verify). No obvious missing functionality like editing or compilation, as verification already includes IR compilation.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Deterministic runtime safety for AI agents: scan PII, gate tool actions, verify LLM output.
Pre-execution governance for AI agents. Deterministic PASS/FAIL/REVIEW verdicts, replayable proof.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
