CSL-Core
Deterministic AI safety policy engine with Z3 formal verification. Write, verify, simulate, and enforce machine-verifiable safety constraints for AI agents. Completely outside the LLM.
README
CSL-Core
CSL-Core (Chimera Specification Language) is a deterministic safety layer for AI agents. Write rules in .csl files, verify them mathematically with Z3, enforce them at runtime — outside the model. The LLM never sees the rules. It simply cannot violate them.
pip install csl-core
Originally built for Project Chimera, now open-source for any AI system.
Why?
prompt = """You are a helpful assistant. IMPORTANT RULES:
- Never transfer more than $1000 for junior users
- Never send PII to external emails
- Never query the secrets table"""
This doesn't work. LLMs can be prompt-injected, rules are probabilistic (99% ≠ 100%), and there's no audit trail when something goes wrong.
CSL-Core flips this: rules live outside the model in compiled, Z3-verified policy files. Enforcement is deterministic — not a suggestion.
Quick Start (60 Seconds)
1. Write a Policy
Create my_policy.csl:
CONFIG {
ENFORCEMENT_MODE: BLOCK
CHECK_LOGICAL_CONSISTENCY: TRUE
}
DOMAIN MyGuard {
VARIABLES {
action: {"READ", "WRITE", "DELETE"}
user_level: 0..5
}
STATE_CONSTRAINT strict_delete {
WHEN action == "DELETE"
THEN user_level >= 4
}
}
2. Verify & Test (CLI)
# Compile + Z3 formal verification
cslcore verify my_policy.csl
# Test a scenario
cslcore simulate my_policy.csl --input '{"action": "DELETE", "user_level": 2}'
# → BLOCKED: Constraint 'strict_delete' violated.
# Interactive REPL
cslcore repl my_policy.csl
3. Use in Python
from chimera_core import load_guard
guard = load_guard("my_policy.csl")
result = guard.verify({"action": "READ", "user_level": 1})
print(result.allowed) # True
result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed) # False
Benchmark: Adversarial Attack Resistance
We tested prompt-based safety rules vs CSL-Core enforcement across 4 frontier LLMs with 22 adversarial attacks and 15 legitimate operations:
| Approach | Attacks Blocked | Bypass Rate | Legit Ops Passed | Latency |
|---|---|---|---|---|
| GPT-4.1 (prompt rules) | 10/22 (45%) | 55% | 15/15 (100%) | ~850ms |
| GPT-4o (prompt rules) | 15/22 (68%) | 32% | 15/15 (100%) | ~620ms |
| Claude Sonnet 4 (prompt rules) | 19/22 (86%) | 14% | 15/15 (100%) | ~480ms |
| Gemini 2.0 Flash (prompt rules) | 11/22 (50%) | 50% | 15/15 (100%) | ~410ms |
| CSL-Core (deterministic) | 22/22 (100%) | 0% | 15/15 (100%) | ~0.84ms |
Why 100%? Enforcement happens outside the model. Prompt injection is irrelevant because there's nothing to inject against. Attack categories: direct instruction override, role-play jailbreaks, encoding tricks, multi-turn escalation, tool-name spoofing, and more.
Full methodology:
benchmarks/
LangChain Integration
Protect any LangChain agent with 3 lines — no prompt changes, no fine-tuning:
from chimera_core import load_guard
from chimera_core.plugins.langchain import guard_tools
from langchain_classic.agents import AgentExecutor, create_tool_calling_agent
guard = load_guard("agent_policy.csl")
# Wrap tools — enforcement is automatic
safe_tools = guard_tools(
tools=[search_tool, transfer_tool, delete_tool],
guard=guard,
inject={"user_role": "JUNIOR", "environment": "prod"}, # LLM can't override these
tool_field="tool" # Auto-inject tool name
)
agent = create_tool_calling_agent(llm, safe_tools, prompt)
executor = AgentExecutor(agent=agent, tools=safe_tools)
Every tool call is intercepted before execution. If the policy says no, the tool doesn't run. Period.
Context Injection
Pass runtime context that the LLM cannot override — user roles, environment, rate limits:
safe_tools = guard_tools(
tools=tools,
guard=guard,
inject={
"user_role": current_user.role, # From your auth system
"environment": os.getenv("ENV"), # prod/dev/staging
"rate_limit_remaining": quota.remaining # Dynamic limits
}
)
LCEL Chain Protection
from chimera_core.plugins.langchain import gate
chain = (
{"query": RunnablePassthrough()}
| gate(guard, inject={"user_role": "USER"}) # Policy checkpoint
| prompt | llm | StrOutputParser()
)
CLI Tools
The CLI is a complete development environment for policies — test, debug, and deploy without writing Python.
verify — Compile + Z3 Proof
cslcore verify my_policy.csl
# ⚙️ Compiling Domain: MyGuard
# • Validating Syntax... ✅ OK
# ├── Verifying Logic Model (Z3 Engine)... ✅ Mathematically Consistent
# • Generating IR... ✅ OK
simulate — Test Scenarios
# Single input
cslcore simulate policy.csl --input '{"action": "DELETE", "user_level": 2}'
# Batch testing from file
cslcore simulate policy.csl --input-file test_cases.json --dashboard
# CI/CD: JSON output
cslcore simulate policy.csl --input-file tests.json --json --quiet
repl — Interactive Development
cslcore repl my_policy.csl --dashboard
cslcore> {"action": "DELETE", "user_level": 2}
🛡️ BLOCKED: Constraint 'strict_delete' violated.
cslcore> {"action": "DELETE", "user_level": 5}
✅ ALLOWED
CI/CD Pipeline
# GitHub Actions
- name: Verify policies
run: |
for policy in policies/*.csl; do
cslcore verify "$policy" || exit 1
done
MCP Server (Claude Desktop / Cursor / VS Code)
Write, verify, and enforce safety policies directly from your AI assistant — no code required.
pip install "csl-core[mcp]"
Add to Claude Desktop config (~/Library/Application Support/Claude/claude_desktop_config.json):
{
"mcpServers": {
"csl-core": {
"command": "uv",
"args": ["run", "--with", "csl-core[mcp]", "csl-core-mcp"]
}
}
}
| Tool | What It Does |
|---|---|
verify_policy |
Z3 formal verification — catches contradictions at compile time |
simulate_policy |
Test policies against JSON inputs — ALLOWED/BLOCKED |
explain_policy |
Human-readable summary of any CSL policy |
scaffold_policy |
Generate a CSL template from plain-English description |
You: "Write me a safety policy that prevents transfers over $5000 without admin approval"
Claude: scaffold_policy → you edit → verify_policy catches a contradiction → you fix → simulate_policy confirms it works
Architecture
┌──────────────────────────────────────────────────────────┐
│ 1. COMPILER .csl → AST → IR → Compiled Artifact │
│ Syntax validation, semantic checks, functor gen │
├──────────────────────────────────────────────────────────┤
│ 2. VERIFIER Z3 Theorem Prover — Static Analysis │
│ Contradiction detection, reachability, rule shadowing │
│ ⚠️ If verification fails → policy will NOT compile │
├──────────────────────────────────────────────────────────┤
│ 3. RUNTIME Deterministic Policy Enforcement │
│ Fail-closed, zero dependencies, <1ms latency │
└──────────────────────────────────────────────────────────┘
Heavy computation happens once at compile-time. Runtime is pure evaluation.
Used in Production
<table> <tr> <td width="80" align="center"> <a href="https://github.com/Chimera-Protocol/Project-Chimera">🏛️</a> </td> <td> <a href="https://github.com/Chimera-Protocol/Project-Chimera"><b>Project Chimera</b></a> — Neuro-Symbolic AI Agent<br/> CSL-Core powers all safety policies across e-commerce and quantitative trading domains. Both are Z3-verified at startup. </td> </tr> </table>
Using CSL-Core? Let us know and we'll add you here.
Example Policies
| Example | Domain | Key Features |
|---|---|---|
agent_tool_guard.csl |
AI Safety | RBAC, PII protection, tool permissions |
chimera_banking_case_study.csl |
Finance | Risk scoring, VIP tiers, sanctions |
dao_treasury_guard.csl |
Web3 | Multi-sig, timelocks, emergency bypass |
python examples/run_examples.py # Run all with test suites
python examples/run_examples.py banking # Run specific example
API Reference
from chimera_core import load_guard, RuntimeConfig
# Load + compile + verify
guard = load_guard("policy.csl")
# With custom config
guard = load_guard("policy.csl", config=RuntimeConfig(
raise_on_block=False, # Return result instead of raising
collect_all_violations=True, # Report all violations, not just first
missing_key_behavior="block" # "block", "warn", or "ignore"
))
# Verify
result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed) # False
print(result.violations) # ['strict_delete']
Full docs: Getting Started · Syntax Spec · CLI Reference · Philosophy
Roadmap
✅ Done: Core language & parser · Z3 verification · Fail-closed runtime · LangChain integration · CLI (verify, simulate, repl) · MCP Server · Production deployment in Chimera v1.7.0
🚧 In Progress: Policy versioning · LangGraph integration
🔮 Planned: LlamaIndex & AutoGen · Multi-policy composition · Hot-reload · Policy marketplace · Cloud templates
🔒 Enterprise (Research): TLA+ temporal logic · Causal inference · Multi-tenancy
Contributing
We welcome contributions! Start with good first issue or check CONTRIBUTING.md.
High-impact areas: Real-world example policies · Framework integrations · Web-based policy editor · Test coverage
License
Apache 2.0 (open-core model). The complete language, compiler, Z3 verifier, runtime, CLI, MCP server, and all examples are open-source. See LICENSE.
Built with ❤️ by Chimera Protocol · Issues · Discussions · Email
推荐服务器
Baidu Map
百度地图核心API现已全面兼容MCP协议,是国内首家兼容MCP协议的地图服务商。
Playwright MCP Server
一个模型上下文协议服务器,它使大型语言模型能够通过结构化的可访问性快照与网页进行交互,而无需视觉模型或屏幕截图。
Magic Component Platform (MCP)
一个由人工智能驱动的工具,可以从自然语言描述生成现代化的用户界面组件,并与流行的集成开发环境(IDE)集成,从而简化用户界面开发流程。
Audiense Insights MCP Server
通过模型上下文协议启用与 Audiense Insights 账户的交互,从而促进营销洞察和受众数据的提取和分析,包括人口统计信息、行为和影响者互动。
VeyraX
一个单一的 MCP 工具,连接你所有喜爱的工具:Gmail、日历以及其他 40 多个工具。
graphlit-mcp-server
模型上下文协议 (MCP) 服务器实现了 MCP 客户端与 Graphlit 服务之间的集成。 除了网络爬取之外,还可以将任何内容(从 Slack 到 Gmail 再到播客订阅源)导入到 Graphlit 项目中,然后从 MCP 客户端检索相关内容。
Kagi MCP Server
一个 MCP 服务器,集成了 Kagi 搜索功能和 Claude AI,使 Claude 能够在回答需要最新信息的问题时执行实时网络搜索。
e2b-mcp-server
使用 MCP 通过 e2b 运行代码。
Neon MCP Server
用于与 Neon 管理 API 和数据库交互的 MCP 服务器
Exa MCP Server
模型上下文协议(MCP)服务器允许像 Claude 这样的 AI 助手使用 Exa AI 搜索 API 进行网络搜索。这种设置允许 AI 模型以安全和受控的方式获取实时的网络信息。