What can you do with this server?

This server provides a full toolkit for writing, analyzing, verifying, and simulating CSL-Core safety policies for AI agents. * Verify CSL policies – Run Z3-based formal verification for syntax, semantics, logical consistency, and IR compilation. * Simulate policy behavior – Test single or batched JSON inputs against a policy to get ALLOWED/BLOCKED results, with optional dry-run mode. * Explain policies – Generate a structured Markdown summary of domains, variables, constraints, and configuration without compiling. * Scaffold new policies – Create ready-to-edit CSL templates from a domain name, plain-English description, and optional variable hints. * Run TLA+ model checking – Perform exhaustive temporal verification with real TLC or a Python BFS fallback, including counterexample traces and fix suggestions. * Analyze policy state space – Inspect variable domains, cardinalities, total state space size, and constraint coverage to plan verification and experiments.

Which integrations are available for this server?

Offers native, drop-in protection for LangChain agents, tools, and chains to enforce external safety constraints that the LLM cannot override. Enforces deterministic safety policies and mathematically proven constraints for AI agents powered by OpenAI models.

de en es ja ko ru zh

CSL-Core

by Chimera-Protocol

Overview Schema Related Servers Score Discussions

Python

Remote

CSL-Core

PyPI version Python License Z3 Verified TLA+ Verified

❤️ Our Contributors!

Contributors

CSL-Core (Chimera Specification Language) is a deterministic safety layer for AI agents. Write rules in .csl files, verify them mathematically with Z3, enforce them at runtime — outside the model. The LLM never sees the rules. It simply cannot violate them.

pip install csl-core

Originally built for Project Chimera, now open-source for any AI system.

Related MCP server: nobulex-mcp-server

Why?

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"""

This doesn't work. LLMs can be prompt-injected, rules are probabilistic (99% ≠ 100%), and there's no audit trail when something goes wrong.

CSL-Core flips this: rules live outside the model in compiled, Z3-verified policy files. Enforcement is deterministic — not a suggestion.

Quick Start (60 Seconds)

1. Write a Policy

Create 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
  }
}

WHEN conditions support AND / OR for compound rules, e.g. WHEN action == "TRANSFER" AND user_tier == "BASIC" — this is what lets a policy be proportional (block writes without blocking reads) instead of an all-or-nothing gate. Full grammar in docs/syntax-spec.md.

2. Verify & Test (CLI)

# 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.csl

3. Use in Python

from 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)  # False

Benchmark: Adversarial Attack Resistance

We tested prompt-based safety rules vs CSL-Core enforcement across 4 frontier LLMs with 22 adversarial attacks and 15 legitimate operations:

Approach	Attacks Blocked	Bypass Rate	Legit Ops Passed	Latency
GPT-4.1 (prompt rules)	10/22 (45%)	55%	15/15 (100%)	~850ms
GPT-4o (prompt rules)	15/22 (68%)	32%	15/15 (100%)	~620ms
Claude Sonnet 4 (prompt rules)	19/22 (86%)	14%	15/15 (100%)	~480ms
Gemini 2.0 Flash (prompt rules)	11/22 (50%)	50%	15/15 (100%)	~410ms
CSL-Core (deterministic)	22/22 (100%)	0%	15/15 (100%)	~0.84ms

Why 100%? Enforcement happens outside the model. Prompt injection is irrelevant because there's nothing to inject against. Attack categories: direct instruction override, role-play jailbreaks, encoding tricks, multi-turn escalation, tool-name spoofing, and more.

Full methodology: benchmarks/

LangChain Integration

Protect any LangChain agent with 3 lines — no prompt changes, no fine-tuning:

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)

Every tool call is intercepted before execution. If the policy says no, the tool doesn't run. Period.

Context Injection

Pass runtime context that the LLM cannot override — user roles, environment, rate limits:

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
    }
)

LCEL Chain Protection

from chimera_core.plugins.langchain import gate

chain = (
    {"query": RunnablePassthrough()}
    | gate(guard, inject={"user_role": "USER"})  # Policy checkpoint
    | prompt | llm | StrOutputParser()
)

CLI Tools

The CLI is a complete development environment for policies — test, debug, and deploy without writing Python.

`verify` — Compile + Z3 Proof

cslcore verify my_policy.csl

# ⚙️  Compiling Domain: MyGuard
#    • Validating Syntax... ✅ OK
#    ├── Verifying Logic Model (Z3 Engine)... ✅ Mathematically Consistent
#    • Generating IR... ✅ OK

`simulate` — Test Scenarios

# 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 --quiet

`repl` — Interactive Development

cslcore repl my_policy.csl --dashboard

cslcore> {"action": "DELETE", "user_level": 2}
🛡️ BLOCKED: Constraint 'strict_delete' violated.

cslcore> {"action": "DELETE", "user_level": 5}
✅ ALLOWED

`formal` — TLA⁺ Model Checking

cslcore formal my_policy.csl

Runs the official TLC model checker (java -jar tla2tools.jar) against your policy. TLC exhaustively explores every reachable state in the abstract state space and proves each temporal property holds — or returns a concrete counterexample trace with the exact state that breaks your invariant.

╔══════════════════════════════════════════════════════════════════════════════╗
║                       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               ║
╚══════════════════════════════════════════════════════════════════════════════╝

Enable in any policy by adding one line to CONFIG:

CONFIG {
  ENFORCEMENT_MODE: BLOCK
  ENABLE_FORMAL_VERIFICATION: TRUE   // ← triggers cslcore formal automatically
}

Or run standalone:

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 Java? CSL-Core falls back to a Python BFS model checker automatically. The banner clearly labels which engine ran. JAR is auto-downloaded on first use (~4MB from the official TLA+ GitHub release).

CI/CD Pipeline

# GitHub Actions
- name: Verify policies
  run: |
    for policy in policies/*.csl; do
      cslcore verify "$policy" || exit 1
    done

MCP Server (Claude Desktop / Cursor / VS Code)

Write, verify, and enforce safety policies directly from your AI assistant — no code required.

pip install "csl-core[mcp]"

Add to Claude Desktop config (~/Library/Application Support/Claude/claude_desktop_config.json):

{
  "mcpServers": {
    "csl-core": {
      "command": "uv",
      "args": ["run", "--with", "csl-core[mcp]", "csl-core-mcp"]
    }
  }
}

Tool	What It Does
`verify_policy`	Z3 formal verification — catches contradictions at compile time
`simulate_policy`	Test policies against JSON inputs — ALLOWED/BLOCKED
`explain_policy`	Human-readable summary of any CSL policy
`scaffold_policy`	Generate a CSL template from plain-English description

You: "Write me a safety policy that prevents transfers over $5000 without admin approval"
Claude: scaffold_policy → you edit → verify_policy catches a contradiction → you fix → simulate_policy confirms it works

Architecture

┌──────────────────────────────────────────────────────────┐
│  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          │
└──────────────────────────────────────────────────────────┘

Heavy computation happens once at compile-time. Runtime is pure evaluation.

Used in Production

Using CSL-Core? Let us know and we'll add you here.

Example Policies

Example	Domain	Key Features
`agent_tool_guard.csl`	AI Safety	RBAC, PII protection, tool permissions
`chimera_banking_case_study.csl`	Finance	Risk scoring, VIP tiers, sanctions
`dao_treasury_guard.csl`	Web3	Multi-sig, timelocks, emergency bypass
`tla_demo.csl`	Formal Methods	TLA⁺ model checking — all properties hold
`tla_demo_violation.csl`	Formal Methods	TLA⁺ counterexample trace + fix suggestions

python examples/run_examples.py          # Run all with test suites
python examples/run_examples.py banking  # Run specific example

API Reference

from 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']

Full docs: Getting Started · Syntax Spec · CLI Reference · Philosophy

Roadmap

✅ Done: Core language & parser · Z3 verification · Fail-closed runtime · LangChain integration · CLI (verify, simulate, repl, formal) · MCP Server · TLA⁺ model checking with real TLC · Predicate abstraction · Counterexample analysis · Production deployment in Chimera v1.7.0

🚧 In Progress: Policy versioning · LangGraph integration

🔮 Planned: LlamaIndex & AutoGen · Multi-policy composition · Hot-reload · Policy marketplace · Cloud templates

🔒 Enterprise (Research): Causal inference · Multi-tenancy

Contributing

We welcome contributions! Start with good first issue or check CONTRIBUTING.md.

High-impact areas: Real-world example policies · Framework integrations · Web-based policy editor · Test coverage

License

Apache 2.0. CSL-Core is intentionally open: the policy language, compiler, Z3 verifier, CLI, MCP server, and all examples are free for any use — commercial, research, or personal. See LICENSE.

This is a deliberate open-core posture. The policy DSL stays open so engineers, researchers, and the broader community can write, share, and verify policies without friction. The commercial layer (Chimera Runtime — production enforcement engine, multi-tenant dashboard, audit infrastructure) is licensed separately.

Trademarks — Chimera Protocol, CSL, and AgentScan are trademarks of Chimera Protocol. Apache 2.0 grants you rights to the code; trademarks are reserved.

For commercial Runtime licensing or partnership inquiries: aytug@chimera-protocol.com

Built with ❤️ by Chimera Protocol · Issues · Discussions · Email

Available Tools

6 tools

explain_policyA

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.

ParametersJSON Schema

Name	Required	Description	Default
`csl_content`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.2/5.0

Behavior3/5

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.

Conciseness5/5

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.

Completeness4/5

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.

Parameters4/5

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.

Purpose5/5

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.

Usage Guidelines4/5

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.

scaffold_policyA

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").

ParametersJSON Schema

Name	Required	Description	Default
`domain_name`	Yes
`description`	Yes
`variables`	No

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.1/5.0

Behavior3/5

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.

Conciseness4/5

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.

Completeness4/5

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.

Parameters4/5

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.

Purpose5/5

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.

Usage Guidelines4/5

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_policyA

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.

ParametersJSON Schema

Name	Required	Description	Default
`csl_content`	Yes
`context_json`	Yes
`dry_run`	No

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.2/5.0

Behavior4/5

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.

Conciseness4/5

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.

Completeness4/5

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.

Parameters5/5

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.

Purpose5/5

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.

Usage Guidelines3/5

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.

tla_verifyA

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.

ParametersJSON Schema

Name	Required	Description	Default
`csl_content`	Yes
`timeout`	No
`use_mock`	No

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.7/5.0

Behavior4/5

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.

Conciseness4/5

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.

Completeness5/5

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.

Parameters5/5

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.

Purpose5/5

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.

Usage Guidelines5/5

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.

universe_infoA

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.

ParametersJSON Schema

Name	Required	Description	Default
`csl_content`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.7/5.0

Behavior4/5

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.

Conciseness4/5

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.

Completeness5/5

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.

Parameters5/5

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.

Purpose5/5

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.

Usage Guidelines5/5

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_policyA

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.

ParametersJSON Schema

Name	Required	Description	Default
`csl_content`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A3.9/5.0

Behavior3/5

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.

Conciseness5/5

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.

Completeness5/5

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.

Parameters4/5

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.

Purpose5/5

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.

Usage Guidelines2/5

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.

Install Server

RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A4.3/5.0

Disambiguation5/5

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).

Naming Consistency4/5

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.

Tool Count5/5

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.

Completeness5/5

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.

Maintenance

ActivityMaintained

ResponsivenessSyncing

Resources

GitHub Repository

Need Help?

Reddit Discussion

Related Servers

Unclaimed servers have limited discoverability.

Looking for Admin?

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

Related MCP Connectors

icme-preflight A
io.github.wyattbenno777
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
AI & Machine Learning Security
142
boundaryai
ai.boundaryai
Deterministic runtime safety for AI agents: scan PII, gate tool actions, verify LLM output.
Security AI & Machine Learning Agent Orchestration
2
governance-platform A
ai.geodesiclabs
Pre-execution governance for AI agents. Deterministic PASS/FAIL/REVIEW verdicts, replayable proof.
AI & Machine Learning Testing & QA Tools Monitoring
373
agentstack-mcp A
io.github.inity13
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
Autonomous Agents Agent Orchestration
241

Related MCP Servers

Aare MCPofficial
Legal & Compliance Autonomous Agents
aare-ai
F
license
Not graded
quality
Not graded
maintenance
Enables formal verification of LLM outputs against compliance ontologies using Z3 SMT solver. Validates that AI-generated content adheres to regulatory requirements like HIPAA or mortgage compliance rules.
Updated 9 months ago (2025-12-04 20:05 UTC)
nobulex-mcp-server
Autonomous Agents Security AI & Machine Learning
arian-gogani
A
license
A
quality
A
maintenance
Proof-of-behavior enforcement for AI agents. Declare behavioral constraints, enforce at runtime, produce SHA-256 hash-chained audit trails. Supports covenants (permit/forbid/require), real-time verification, and cross-agent trust handshakes.
Updated a month ago (2026-08-03 22:50 UTC)
4
39
MIT
hejdar-mcp
Autonomous Agents Security
ARKALDA
A
license
A
quality
D
maintenance
Runtime policy enforcement for AI agents. Evaluate every agent action against your organization's policies before execution, with observe and enforce modes.
Updated 5 months ago (2026-04-15 19:06 UTC)
1
1
MIT
QWED-MCPofficial
Code Execution Code Analysis
QWED-AI
A
license
B
quality
A
maintenance
Enables deterministic verification for AI assistants by executing Python code that uses symbolic engines like SymPy and Z3 for math, logic, and code analysis.
Updated 8 days ago (2026-08-27 08:48 UTC)
2
Apache 2.0

Latest Blog Posts

Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)
By Om-Shree-0709 on July 25, 2026.
mcp
Agent Identity
OAuth 2.1
Your AI Chatbot Just Exposed Your CEO's Salary to an Intern
By Om-Shree-0709 on July 2, 2026.
Agent Identity
MCP Security
OAuth Delegation
Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)
By Om-Shree-0709 on June 30, 2026.
Agentic Ai
Prompt Injection
WebAssembly

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/Chimera-Protocol/csl-core'

If you have feedback or need assistance with the MCP directory API, please join our Discord server

CSL-Core

❤️ Our Contributors!

Why?

Quick Start (60 Seconds)

1. Write a Policy

2. Verify & Test (CLI)

3. Use in Python

Benchmark: Adversarial Attack Resistance

LangChain Integration

Context Injection

LCEL Chain Protection

CLI Tools

verify — Compile + Z3 Proof

simulate — Test Scenarios

repl — Interactive Development

formal — TLA⁺ Model Checking

CI/CD Pipeline

MCP Server (Claude Desktop / Cursor / VS Code)

Architecture

Used in Production

Example Policies

API Reference

Roadmap

Contributing

License

Available Tools

Output Schema

Output Schema

Output Schema

Output Schema

Output Schema

Output Schema

Maintenance

Resources

Looking for Admin?

Related MCP Connectors

Related MCP Servers

Aare MCPofficial

QWED-MCPofficial

Latest Blog Posts

MCP directory API

`verify` — Compile + Z3 Proof

`simulate` — Test Scenarios

`repl` — Interactive Development

`formal` — TLA⁺ Model Checking