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"""プロンプトによる安全対策は機能しません。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%) | ~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に1行追加することで有効化します：
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+ ToolboxJavaがない場合？ CSL-Coreは自動的にPythonのBFSモデルチェッカーにフォールバックします。バナーにはどのエンジンが実行されたかが明確に表示されます。JARは初回使用時に自動的にダウンロードされます（公式TLA+ GitHubリリースから約4MB）。
# GitHub Actions
- name: Verify policies
run: |
for policy in policies/*.csl; do
cslcore verify "$policy" || exit 1
doneAIアシスタントから直接安全ポリシーを記述、検証、強制します。コードは不要です。
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をご利用ですか？お知らせいただければこちらに追加いたします。
例 | ドメイン | 主な機能 |
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']完全なドキュメント： Getting Started · Syntax Spec · CLI Reference · Philosophy
✅ 完了: コア言語とパーサー · 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を参照してください。
Built with ❤️ by 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.
