CSL-Core (Chimera Specification Language) 是一个用于 AI 智能体的确定性安全层。在 .csl 文件中编写规则，使用 Z3 进行数学验证，并在运行时强制执行——完全在模型之外。LLM 永远看不到这些规则，但它绝对无法违反它们。
pip install csl-core最初为 Project Chimera 构建，现已开源，适用于任何 AI 系统。
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"""仅靠提示词（Prompt）是不够的。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我们针对 4 个前沿 LLM，使用 22 种对抗性攻击和 15 种合法操作，对比了基于提示词的安全规则与 CSL-Core 的强制执行效果：
方法 | 拦截攻击数 | 绕过率 | 通过合法操作数 | 延迟 |
GPT-4.1 (提示词规则) | 10/22 (45%) | 55% | 15/15 (100%) | ~850ms |
GPT-4o (提示词规则) | 15/22 (68%) | 32% | 15/15 (100%) | ~620ms |
Claude Sonnet 4 (提示词规则) | 19/22 (86%) | 14% | 15/15 (100%) | ~480ms |
Gemini 2.0 Flash (提示词规则) | 11/22 (50%) | 50% | 15/15 (100%) | ~410ms |
CSL-Core (确定性) | 22/22 (100%) | 0% | 15/15 (100%) | ~0.84ms |
为什么是 100%？ 因为强制执行发生在模型之外。提示词注入攻击无效，因为根本没有可供注入的目标。攻击类别包括：直接指令覆盖、角色扮演越狱、编码技巧、多轮升级、工具名称欺骗等。
完整方法论：
benchmarks/
只需 3 行代码即可保护任何 LangChain 智能体——无需更改提示词，无需微调：
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 — 编译 + Z3 证明cslcore 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 文件在首次使用时会自动下载（约 4MB，来自官方 TLA+ GitHub 发布版）。
# GitHub Actions
- name: Verify policies
run: |
for policy in policies/*.csl; do
cslcore verify "$policy" || exit 1
done直接从您的 AI 助手编写、验证和强制执行安全策略——无需代码。
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 输入测试策略——返回 ALLOWED/BLOCKED |
| 任何 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？请告诉我们，我们将把您加入列表。
示例 | 领域 | 关键特性 |
AI 安全 | 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 服务器 · 基于真实 TLC 的 TLA⁺ 模型检查 · 谓词抽象 · 反例分析 · Chimera v1.7.0 生产部署
🚧 进行中： 策略版本控制 · LangGraph 集成
🔮 计划中： LlamaIndex & AutoGen · 多策略组合 · 热重载 · 策略市场 · 云端模板
🔒 企业级 (研究中)： 因果推理 · 多租户
欢迎贡献！从 good first issue 开始，或查看 CONTRIBUTING.md。
高影响力领域： 真实世界的策略示例 · 框架集成 · 基于 Web 的策略编辑器 · 测试覆盖率
Apache 2.0 (开放核心模型)。完整的语言、编译器、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.
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.
