CSL-Core

❤️ Our Contributors!

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

pip install csl-core

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

Why?

prompt = """You are a helpful assistant. IMPORTANT RULES:
- Never transfer more than $1000 for junior users
- Never send PII to external emails
- Never query the secrets table"""

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

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

Quick Start (60 Seconds)

1. Write a Policy

Create my_policy.csl:

CONFIG {
  ENFORCEMENT_MODE: BLOCK
  CHECK_LOGICAL_CONSISTENCY: TRUE
}

DOMAIN MyGuard {
  VARIABLES {
    action: {"READ", "WRITE", "DELETE"}
    user_level: 0..5
  }

  STATE_CONSTRAINT strict_delete {
    WHEN action == "DELETE"
    THEN user_level >= 4
  }
}

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

2. Verify & Test (CLI)

# Compile + Z3 formal verification
cslcore verify my_policy.csl

# Test a scenario
cslcore simulate my_policy.csl --input '{"action": "DELETE", "user_level": 2}'
# → BLOCKED: Constraint 'strict_delete' violated.

# Interactive REPL
cslcore repl my_policy.csl

3. Use in Python

from chimera_core import load_guard

guard = load_guard("my_policy.csl")

result = guard.verify({"action": "READ", "user_level": 1})
print(result.allowed)  # True

result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed)  # False

Venom: discover, write, map, watch (0.6)

Writing a policy assumes you already know which agents you run, what they can reach and how their real tool calls map onto policy variables. Venom makes that part of the tool.

pip install csl-core
cslcore venom          # read-only discovery of every AI agent on this machine
cslcore setup          # guided: findings, policies, mapping, enforcement mode, wiring
cslcore studio         # write and verify policies in the terminal (Z3, TLA+), bind agents, go live
cslcore watch          # live management panel

cslcore venom reads code (parsed, never run), assistant and MCP configs, cron / systemd / launchd, the process list, run history metadata and existing .csl policies. Credential values, prompt text and transcripts never reach any output. On a test host it looks like this:

╭─  CSL-Core Venom 0.6.0  ─────────────────────────────────────────────────────╮
│ ops-01 · linux · 2026-10-01 14:22 · 0.4s · fixture host · read-only          │
╰──────────────────────────────────────────────────────────────────────────────╯
  Discovery   ✓ code  ✓ config  ✓ triggers  ✓ runtime  ✓ history  ✓ policies
              5 files · 1 parse error · 0 paths not readable

  AGENTS      6 total   ● 4 running   ○ 1 stopped   ◷ 1 scheduled

  Agent               State         Runs 7d Tools   Top access     Guard     
  claude-code:sandbox ● running         n/a     9   EXEC  Bash     none      
  ingest-worker       ● running           7     4   EXEC  run_com… none      
  publisher           ◷ daily 06:00     n/a     2   EXT   post_to… none      
  claude-code:ops     ● running           3    29   EXEC  Bash     no rule   
  membership-bot      ○ stopped         n/a     2   SPEND transfe… wrapper   
  rogue/agent.py      ● running         n/a     0   -              none      

  COVERAGE    █░░░░░░░░░░░░░░░    4%   2 of 46 tools guarded · 29 no rule

  FINDINGS    ▲ 5 high   ■ 8 medium   ● 1 low
   ▲ V01  ingest-worker runs as root
   ▲ V02  claude-code:sandbox can execute commands without a guard (Bash)
   ▲ V02  ingest-worker can execute commands without a guard (run_command)
   ▲ V03  permission prompts are disabled for claude-code:sandbox
   ▲ V04  publisher: inbound messaging (/webhooks/sms) reaches EXTERNAL tool p…
          9 more in the report

  NEXT        cslcore policy fix  apply drift suggestions, shown as a diff first

cslcore setup then walks through ten resumable steps:

1. Findings: V01 to V16, from "agent runs as root" to "inbound webhook reaches a public posting tool".
2. Policies: per agent, a deterministic draft from risk-class templates, or a draft written by your own assistant through the MCP tools below. Every draft passes the same gate (parse, validate, Z3, diff, your confirmation) before it becomes active.
3. Mapping: generated mappings use the fail-closed helpers in chimera_core.mapping (to_enum, to_flag, to_range), and a mapping test pushes case variants, unknown values, missing keys, wrong types and range edges through mapping and guard. Any malformed input that ends in ALLOW is reported as fail-open. Every derived check (path in scope, command allowlisted, destination allowed) also gets bypass tricks: traversal, prefix folders, command chaining and substitution, credentials and suffix hosts in URLs, and more, each built so the right answer is known. It works on hand-written mappings too, with your red-team findings kept as regression cases: cslcore map --agent NAME --test --mapping my_mapper.py:classify --classify path_ok=scope:file_path --allowed-root /srv/app. The hardened classifiers in_scope, command_allowed and destination_allowed pass every trick family. Guide: docs/venom/MAPPING.md.
4. Enforcement mode: log (nothing blocked, every decision recorded as ALLOW or WOULD BLOCK) or block, per agent.
5. Wiring: a snippet per framework (Python, LangChain, Claude Code PreToolUse hook via cslcore hook).

cslcore studio is the policy editor, inside the terminal. It opens on its own, from setup's policy step (w), from the watch panel (o on a rule) and from the cslcore studio --agent NAME line the scan suggests. One policy per session (Ctrl+O switches, Ctrl+N starts a new one):

• F5 runs Z3 (contradictions between rules, rules that can never trigger) and F8 runs TLA+ (real TLC when Java and tla2tools.jar are available, the built-in model checker otherwise), each with its own animation of what the engine is checking. Nothing is verified on save.
• Suggestions come from Z3, TLA+ and the agents themselves (tool names the policy does not know, risky tools without a rule) and apply to the text with Enter.
• The Agents tab shows the fit per bound agent (tools covered, mapping test, fail-open cases) and replays the agent's recorded decisions against the edited text: how many calls would now be blocked or allowed, before anything changes.
• Ctrl+B binds agents to the policy, one or many at once (filter, then Enter selects every match). One policy can guard many agents; each gets its own fail-closed mapping. Bindings live in .csl/venom/state.json and running guards created with venom_guard(agent) follow them.
• Ctrl+L goes live: it requires a current Z3 pass, keeps the previous version in .csl/venom/history/, writes the policy, binds the selected agents, and running guards switch on their next call. Editing a live policy works on a draft until you go live again.

Already on 0.5.1? Upgrading changes nothing; cslcore setup recognises your integration, keeps your policies in place and tests your own mapper for fail-open cases. See docs/venom/MIGRATION.md. Try the whole flow on a sample host: cslcore setup --root tests/venom/fixtures/host_ops --workspace /tmp/venom-demo, then python scripts/venom_demo_traffic.py --workspace /tmp/venom-demo and cslcore watch --workspace /tmp/venom-demo.

cslcore watch is the management panel: agents with their mode and block rate, the live decision stream, and rules ranked by how often they would block (the ones to tune before switching to block). Keys: m switches an agent between log and block, d disables an agent (kill switch, blocks every action in any mode), Enter opens its tools so single tools can be disabled or exempted, Tab moves to the rules so a rule that blocks too often can be relaxed for one agent (re-verified, previous version kept), / searches, Esc goes back, M switches every agent at once. Changes reach running agents on their next tool call, without a restart, and are recorded in .csl/venom/audit.jsonl. The same controls exist on the command line: cslcore mode.

Other commands: cslcore venom report --agent NAME, cslcore policy list|show|new|edit|extend|fix|verify|diff|activate, cslcore exempt add|list|approve|remove (exemptions need a reason and an approver and are encoded in the verified policy), cslcore venom --check for CI (exit 3 on high findings or vocabulary drift), and --probe to ask configured MCP servers for their real tool lists. Optional: pip install "csl-core[venom]" adds psutil for process discovery.

0.5.1 behavior is unchanged. A contract suite generated from the v0.5.1 tag (public API, CLI output, MCP tools and outputs, policy hashes, thousands of guard decisions) runs first in CI, together with the unmodified v0.5.1 test suite.

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 (run 2026-02-18, model versions as of that date — re-run pending against current models):

CSL-Core's own runtime hot path (ChimeraGuard.verify(), no compilation) measured in isolation is sub-0.1ms even at 40 compiled rules — see paper/PAPER_FACTS.md for the full methodology and per-size breakdown.

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

Full methodology: benchmarks/

LangChain Integration

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

from chimera_core import load_guard
from chimera_core.plugins.langchain import guard_tools
from langchain_classic.agents import AgentExecutor, create_tool_calling_agent

guard = load_guard("agent_policy.csl")

# Wrap tools — enforcement is automatic
safe_tools = guard_tools(
    tools=[search_tool, transfer_tool, delete_tool],
    guard=guard,
    inject={"user_role": "JUNIOR", "environment": "prod"},  # LLM can't override these
    tool_field="tool"  # Auto-inject tool name
)

agent = create_tool_calling_agent(llm, safe_tools, prompt)
executor = AgentExecutor(agent=agent, tools=safe_tools)

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

Context Injection

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

safe_tools = guard_tools(
    tools=tools,
    guard=guard,
    inject={
        "user_role": current_user.role,         # From your auth system
        "environment": os.getenv("ENV"),        # prod/dev/staging
        "rate_limit_remaining": quota.remaining # Dynamic limits
    }
)

LCEL Chain Protection

from chimera_core.plugins.langchain import gate

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

CLI Tools

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

verify — Compile + Z3 Proof

cslcore verify my_policy.csl

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

simulate — Test Scenarios

# Single input
cslcore simulate policy.csl --input '{"action": "DELETE", "user_level": 2}'

# Batch testing from file
cslcore simulate policy.csl --input-file test_cases.json --dashboard

# CI/CD: JSON output
cslcore simulate policy.csl --input-file tests.json --json --quiet

repl — Interactive Development

cslcore repl my_policy.csl --dashboard

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

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

formal — TLA⁺ Model Checking

cslcore formal my_policy.csl

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

╔══════════════════════════════════════════════════════════════════════════════╗
║                       TLA⁺ FORMAL VERIFICATION ENGINE                        ║
║          Chimera Specification Language · Temporal Logic of Actions          ║
║                                                                              ║
║    ⚡  REAL TLC  ·  java -jar tla2tools.jar  ·  Exhaustive Model Checking    ║
║       TLC2 Version 2026.03.31.154134 (rev: becec35)  ·  pid 48146  ·  1      ║
║                                  worker(s)                                   ║
╚══════════════════════════════════════════════════════════════════════════════╝

  Variable      Domain                         Cardinality
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
  agent_tier    {"STANDARD", "PREMIUM"}                |2|
  task_type     {"READ", "WRITE", "ANALYZE"}           |3|
  risk_score    0..5                                   |6|

  ├─ □(no_destructive_ops)      ✅  HOLDS  [288 states  349ms]
  ├─ □(no_production_access)    ✅  HOLDS  [288 states  349ms]
  ├─ □(bounded_risk)            ✅  HOLDS  [288 states  349ms]

  └─ Proof hash: 17dd1564897d242fc045a3a884a52bbb… ✅

╔══════════════ TLA⁺ VERIFICATION COMPLETE — ALL PROPERTIES HOLD ══════════════╗
║  ✅  Domain: AIAgentSafetyDemo  ·  ⬡ 144 states  ·  ⏱ 1047ms               ║
╚══════════════════════════════════════════════════════════════════════════════╝

Enable in any policy by adding one line to CONFIG:

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

Or run standalone:

cslcore formal policy.csl              # real TLC (Java required, JAR auto-downloaded)
cslcore formal policy.csl --mock       # Python BFS fallback (no Java needed)
cslcore formal policy.csl --timeout 120
cslcore formal policy.csl --export-tla ./specs/   # save .tla + .cfg for TLA+ Toolbox

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

CI/CD Pipeline

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

MCP Server (Claude Desktop / Cursor / VS Code)

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

pip install "csl-core[mcp]"

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

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

You: "Write me a safety policy that prevents transfers over $5000 without admin approval"

Claude: scaffold_policy → you edit → verify_policy catches a contradiction → you fix → simulate_policy confirms it works

Architecture

┌──────────────────────────────────────────────────────────┐
│  1. COMPILER    .csl → AST → IR → Compiled Artifact      │
│     Syntax validation, semantic checks, functor gen       │
├──────────────────────────────────────────────────────────┤
│  2. Z3 VERIFIER    Theorem Prover — Static Analysis       │
│     Contradiction detection, reachability, rule shadowing │
│     ⚠️ If verification fails → policy will NOT compile    │
├──────────────────────────────────────────────────────────┤
│  3. TLA⁺ VERIFIER  Model Checker — Temporal Safety        │
│     Exhaustive state-space exploration via TLC            │
│     Predicate abstraction for large numeric domains       │
│     Counterexample traces + automated fix suggestions     │
│     (opt-in: ENABLE_FORMAL_VERIFICATION: TRUE)            │
├──────────────────────────────────────────────────────────┤
│  4. RUNTIME     Deterministic Policy Enforcement          │
│     Fail-closed, zero dependencies, <1ms latency          │
└──────────────────────────────────────────────────────────┘

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

Used in Production

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

Example Policies

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

API Reference

from chimera_core import load_guard, RuntimeConfig

# Load + compile + verify
guard = load_guard("policy.csl")

# With custom config
guard = load_guard("policy.csl", config=RuntimeConfig(
    raise_on_block=False,          # Return result instead of raising
    collect_all_violations=True,   # Report all violations, not just first
    missing_key_behavior="block"   # "block", "warn", or "ignore"
))

# Verify
result = guard.verify({"action": "DELETE", "user_level": 2})
print(result.allowed)     # False
print(result.violations)  # ['strict_delete']

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

Roadmap

✅ Done: Core language & parser · Z3 verification · Fail-closed runtime · LangChain integration · CLI (verify, simulate, repl, formal) · MCP Server · TLA⁺ model checking with real TLC · Predicate abstraction · Counterexample analysis · Production deployment in Chimera v1.7.0 · Venom: agent discovery, policy workbench, fail-closed mapping test, live management panel (0.6)

🚧 In Progress: Policy versioning · LangGraph integration

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

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

Contributing

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

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

License

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

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

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

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

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