CSL-Core (Chimera Specification Language) — это детерминированный уровень безопасности для ИИ-агентов. Пишите правила в файлах .csl, проверяйте их математически с помощью Z3, обеспечивайте их соблюдение во время выполнения — вне модели. LLM никогда не видит эти правила. Она просто не может их нарушить.
pip install csl-coreИзначально создано для Project Chimera, теперь с открытым исходным кодом для любой системы ИИ.
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"""Это не работает. LLM подвержены промпт-инъекциям, правила носят вероятностный характер (99% ≠ 100%), и нет аудиторского следа, когда что-то идет не так.
CSL-Core меняет подход: правила находятся вне модели в скомпилированных, проверенных Z3 файлах политик. Принудительное исполнение является детерминированным — это не рекомендация.
Создайте 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) # FalseМы протестировали правила безопасности на основе промптов против принудительного исполнения CSL-Core на 4 передовых LLM с использованием 22 состязательных атак и 15 легитимных операций:
Подход | Заблокировано атак | Уровень обхода | Пройдено легитимных операций | Задержка |
GPT-4.1 (промпт-правила) | 10/22 (45%) | 55% | 15/15 (100%) | ~850мс |
GPT-4o (промпт-правила) | 15/22 (68%) | 32% | 15/15 (100%) | ~620мс |
Claude Sonnet 4 (промпт-правила) | 19/22 (86%) | 14% | 15/15 (100%) | ~480мс |
Gemini 2.0 Flash (промпт-правила) | 11/22 (50%) | 50% | 15/15 (100%) | ~410мс |
CSL-Core (детерминированный) | 22/22 (100%) | 0% | 15/15 (100%) | ~0.84мс |
Почему 100%? Принудительное исполнение происходит вне модели. Промпт-инъекция не имеет значения, потому что нет ничего, против чего можно было бы совершить инъекцию. Категории атак: прямое переопределение инструкций, джейлбрейки через ролевые игры, трюки с кодированием, эскалация в несколько шагов, подмена имен инструментов и многое другое.
Полная методология:
benchmarks/
Защитите любого агента LangChain с помощью 3 строк — никаких изменений промптов, никакого дообучения:
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)Каждый вызов инструмента перехватывается до выполнения. Если политика запрещает, инструмент не запускается. Точка.
Передавайте контекст выполнения, который LLM не может переопределить — роли пользователей, окружение, лимиты запросов:
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()
)CLI — это полноценная среда разработки для политик: тестируйте, отлаживайте и развертывайте без написания кода на Python.
verify — Компиляция + доказательство Z3cslcore verify my_policy.csl
# ⚙️ Compiling Domain: MyGuard
# • Validating Syntax... ✅ OK
# ├── Verifying Logic Model (Z3 Engine)... ✅ Mathematically Consistent
# • Generating IR... ✅ OKsimulate — Тестовые сценарии# 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 — Интерактивная разработкаcslcore repl my_policy.csl --dashboard
cslcore> {"action": "DELETE", "user_level": 2}
🛡️ BLOCKED: Constraint 'strict_delete' violated.
cslcore> {"action": "DELETE", "user_level": 5}
✅ ALLOWEDformal — Модельная проверка TLA⁺cslcore formal my_policy.cslЗапускает официальный инструмент проверки моделей TLC (java -jar tla2tools.jar) для вашей политики. TLC исчерпывающе исследует каждое достижимое состояние в пространстве абстрактных состояний и доказывает, что каждое временное свойство соблюдается — или возвращает конкретный контрпример с точным состоянием, которое нарушает ваш инвариант.
╔══════════════════════════════════════════════════════════════════════════════╗
║ 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 ║
╚══════════════════════════════════════════════════════════════════════════════╝Включите в любой политике, добавив одну строку в CONFIG:
CONFIG {
ENFORCEMENT_MODE: BLOCK
ENABLE_FORMAL_VERIFICATION: TRUE // ← triggers cslcore formal automatically
}Или запустите отдельно:
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Нет Java? CSL-Core автоматически переключается на Python-реализацию проверки моделей BFS. Баннер четко указывает, какой движок был запущен. JAR скачивается автоматически при первом использовании (~4 МБ из официального релиза TLA+ на GitHub).
# GitHub Actions
- name: Verify policies
run: |
for policy in policies/*.csl; do
cslcore verify "$policy" || exit 1
doneПишите, проверяйте и обеспечивайте соблюдение политик безопасности прямо из вашего ИИ-ассистента — код не требуется.
pip install "csl-core[mcp]"Добавьте в конфигурацию Claude Desktop (~/Library/Application Support/Claude/claude_desktop_config.json):
{
"mcpServers": {
"csl-core": {
"command": "uv",
"args": ["run", "--with", "csl-core[mcp]", "csl-core-mcp"]
}
}
}Инструмент | Что он делает |
| Формальная верификация Z3 — обнаруживает противоречия на этапе компиляции |
| Тестирование политик на входных данных JSON — РАЗРЕШЕНО/ЗАБЛОКИРОВАНО |
| Понятное человеку резюме любой политики CSL |
| Генерация шаблона CSL на основе описания на обычном английском |
Вы: "Напиши мне политику безопасности, которая предотвращает переводы свыше $5000 без одобрения администратора"
Claude: scaffold_policy → вы редактируете → verify_policy обнаруживает противоречие → вы исправляете → simulate_policy подтверждает работу
┌──────────────────────────────────────────────────────────┐
│ 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 │
└──────────────────────────────────────────────────────────┘Тяжелые вычисления выполняются один раз на этапе компиляции. Время выполнения — это чистая оценка.
Используете CSL-Core? Дайте нам знать, и мы добавим вас сюда.
Пример | Домен | Ключевые особенности |
Безопасность ИИ | RBAC, защита PII, разрешения инструментов | |
Финансы | Скоринг рисков, VIP-уровни, санкции | |
Web3 | Мультиподпись, временные блокировки, аварийный обход | |
Формальные методы | Модельная проверка TLA⁺ — все свойства соблюдаются | |
Формальные методы | Контрпример TLA⁺ + предложения по исправлению |
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']Полная документация: Начало работы · Спецификация синтаксиса · Справочник CLI · Философия
✅ Сделано: Базовый язык и парсер · Верификация Z3 · Среда выполнения с отказом по умолчанию · Интеграция с LangChain · CLI (verify, simulate, repl, formal) · MCP-сервер · Модельная проверка TLA⁺ с реальным TLC · Абстракция предикатов · Анализ контрпримеров · Развертывание в продакшене в Chimera v1.7.0
🚧 В процессе: Версионирование политик · Интеграция с LangGraph
🔮 Планируется: LlamaIndex и AutoGen · Композиция нескольких политик · Горячая перезагрузка · Маркетплейс политик · Облачные шаблоны
🔒 Enterprise (исследования): Причинно-следственный вывод · Мультиарендность
Мы приветствуем вклад! Начните с good first issue или ознакомьтесь с CONTRIBUTING.md.
Области с высоким влиянием: Реальные примеры политик · Интеграции с фреймворками · Веб-редактор политик · Покрытие тестами
Apache 2.0 (open-core модель). Весь язык, компилятор, верификатор Z3, среда выполнения, CLI, MCP-сервер и все примеры имеют открытый исходный код. См. LICENSE.
Создано с ❤️ компанией Chimera Protocol · Issues · Discussions · Email
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. Dates show when Glama detected each change.
v0.1.0explain_policyscaffold_policysimulate_policytla_verifyuniverse_infoverify_policyEach 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.
Unclaimed servers have limited discoverability.
If you are the server author, to access and configure the admin panel.
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.
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
