This MCP server lets an AI assistant verify, simulate, explain, scaffold, and formally analyze CSL policies, inspect Venom-discovered agents, and save drafts/propose exemptions while the operator keeps activation control.
verify_policy — Z3-check a CSL policy for syntax, semantics, logical consistency, conflicts, and compile IR.
simulate_policy — Run a policy against one or many JSON inputs; returns ALLOWED/BLOCKED, violations, and dry-run shadow testing.
explain_policy — Parse a policy and return a structured Markdown summary of domain, variables, constraints, and config.
scaffold_policy — Generate an editable .csl policy template from a description, domain name, and optional variable hints.
tla_verify — Run TLA+/TLC model checking for exhaustive temporal safety, state counts, counterexample traces, and fix suggestions.
universe_info — Analyze a policy's state space: variable domains, cardinalities, total size, constraints, and coverage.
venom_inventory — Summarize AI agents Venom discovered on the machine: kind, state, tool count, risk class, guard status, coverage, findings.
venom_agent — Show one discovered agent in detail: tools, parameters, risk classes, triggers, guard status, and policy agent key.
venom_policy_context — Get everything needed to draft/revise one agent's policy: active/draft policy, findings, drift, valid-draft rules.
venom_save_draft — Verify and save a CSL draft to .csl/venom/drafts/; it never activates the policy.
venom_propose_exemption — Propose an agent/tool guarding exemption with a reason; recorded as proposed, operator approves in CLI.
Safety limits: redacted outputs, no credential values/prompts, drafts not activated, exemptions not approved.
Find, prove and control the AI agents on your machines.
CSL-Core finds every AI agent on a host and what it can reach, writes a policy for each one, proves the policies with Z3 and TLA+, tests the code that connects agents to policies against bypass tricks, and enforces them deterministically, outside the model. The model never sees the rules, so it cannot talk its way past them.
pip install csl-core
cslcore setupcslcore setup is the whole first install: it scans the machine, explains what it found, and opens
the protection board, the riskiest agents first. Enter gives every agent standard limits, a policy
made from them and checked with Z3, and the change that puts the guard in its call path, shown as a
diff with a one-line summary before anything is written. A number opens one agent instead: its
limits in your own numbers (amounts, any numeric argument, allow, approval or block per tool), the
policy, the wiring and a check that decides sample calls with the real policy and shows what runs
and what stops. Until you confirm a wiring change it writes only inside the folder you run it in.
It is resumable at any step, and cslcore setup later opens the board where you left it.
Then watch it run:
cslcore watchWant to look first, without installing anything? With uv:
uvx csl-core venomThe scan on its own: read-only, about a second. Add --share to get a card of your machine's reach
map to post (no host name, user names or paths on it; --anonymize also hides agent names). To try
the whole flow on a sample host instead of your machine, from a clone of this repository (the sample
host and the traffic script are in the repository, not in the package):
cslcore setup --root tests/venom/fixtures/host_ops --workspace /tmp/csl-demo
python scripts/venom_demo_traffic.py --workspace /tmp/csl-demo
cslcore watch --workspace /tmp/csl-demoAlready on 0.5.1? Upgrading changes nothing: setup recognises your integration, keeps your policies where they are and tests your own mapper. See MIGRATION.md.
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"""Rules in a prompt are suggestions. Models can be talked out of them, they hold most of the time rather than every time, and nothing records what happened. CSL-Core keeps the rules outside the model, in compiled policies that are proven consistent before they run and checked on every tool call, the same way every time.
Three things usually go wrong before a single rule is written, and CSL-Core covers them too:
Nobody knows which agents are running. Assistants, MCP servers, scheduled jobs and scripts with tool access accumulate on every machine.
The policy is proven, the glue code is not. The code that turns a real call like
Write(file_path="/srv/app/../etc/passwd") into policy variables is where guards are bypassed.
Strict rules break real work. Switching enforcement on without seeing what it would block gets it switched off again.
cslcore venomReads code (parsed, never run), assistant and MCP configs, cron, systemd and launchd, the process
list, run history and existing policies. Every agent gets its tools classified by risk (read,
write, external, execute, spend, destructive), its guard coverage, and findings from "agent runs as
root" to "an inbound webhook reaches a public posting tool". Nothing on the host is changed;
credential values, prompts and transcripts never reach any output. Reports land in
.csl/venom/reports/, and cslcore venom --check gates CI. A scan is a snapshot, so each later
scan also names what opened since the last one (a plugin installed, a credential added);
--check --fail-on-new-reach fails CI on it. Between scans the guard covers the gap: a tool it
was not mapped for is denied, not allowed.
When discovery finishes, the web draws back into one point and spreads again along what can really reach what: the reach map, with the strongest chain lit as a purple artery.
cslcore venom mapEach agent on its own may look harmless. The risk is in the chain: an agent that reads web content can change the code of another agent that runs as root, or holds a cloud credential, or moves money. Venom builds the reach graph from what discovery found (who receives untrusted input, whose declared file scope or account covers whose files, who runs as root, which tools have no rule) and finds the chains that escalate: routes through two or more agents to something none of the earlier agents could do on its own. A tool with an active rule breaks the chain.
cslcore venom map opens it full screen:
Select with the arrows or jump with 1 to 9; the panel shows what reaches the node and what
it reaches.
Enter dives into an agent: its tools on a ring, and what each tool reaches.
s turns the map into a 3D globe that brings the selected node to the front; n hides the
names, r replays the spread.
The strongest chain is also on the scan screen and in the reports, step by step with its evidence. On a host without chains, the most serious direct exposure is shown instead (for example an assistant that reads web content and runs commands without a rule).
cslcore setupTen resumable steps: scope, discovery, inventory, findings with what to do about each, exemptions,
policies (the protection board), verification, mapping, enforcement mode and wiring, activation. On
the board each agent shows its limits, policy, wiring, mode and check; Enter gives the agents
without a policy standard protection, a number runs one agent's loop, s leaves an agent untouched,
and o offers the other ways: keep the policy it already uses, write it in the studio or an editor,
or let your own assistant draft it. Every policy passes the same gate (parse, validate, Z3, the
mapping test) before it becomes active. An agent activated for the first time starts in block mode
unless you chose log; agents already running in log mode keep it. Setup ends with the check per
agent and the commands that undo or loosen each step.
Then the guard goes into each agent's call path for real, once its policy is active: setup shows the
change as a diff and makes it when you confirm (--wire with --yes), or later cslcore wire.
Claude Code: a PreToolUse hook in the project's .claude/settings.local.json. Every tool
call goes through it, including tools a plugin adds later.
Python tools (LangChain @tool, OpenAI Agents @function_tool, CrewAI, plain functions):
@_csl_guard.tool("name") directly above each tool function, under the framework's own decorator.
The tool keeps its name, docstring and signature, so the framework sees the same tool.
Before a Python agent is wired, setup checks that the interpreter it runs with (its project's
virtual environment, when it has one) can import csl-core, and offers the install command if not.
The guard line finds its workspace relative to the agent's file, through CSL_WORKSPACE, or in the
nearest .csl folder above it, so the line holds in a clone, in CI and on a server once
cslcore apply has made .csl/ there from csl-limits.ini (the one file to commit).
Keep the workspace on a local disk: file locks are not reliable on NFS and some container volumes.
A tool that exists only as a schema (the model asks for it, your own code runs it) cannot be wired
automatically; it gets the exact guard.check line instead, and the summary says it is not wired.
Each changed file is copied into the workspace first, and cslcore wire --undo puts it back. The
map and the live panel only show an agent as guarded when the scan sees its guard in the call path;
x on an agent nothing guards yet offers to put it under one, then freezes it.
Limits, in your own numbers. cslcore limits shows and changes what each agent may do
(--set transfer_funds=100k..300k, --set export_rows.limit=..1000, --decide delete_user=block),
makes the policy again, checks it and runs the check. A repository can keep them in
csl-limits.ini, reviewed in pull requests: cslcore apply makes them active, and
cslcore apply --check in CI fails when a policy made from the file would not hold.
Approvals are real. A call over the free amount does not simply stop: Claude Code asks you
(the hook answers "ask"), and a wired Python tool returns ApprovalPending and waits in
cslcore watch (key a); once you approve it there, the same call runs once within ten minutes.
What no approval can allow (above the maximum, a destructive command) still stops.
cslcore studioA full policy editor in the terminal. F5 (or Ctrl+R) runs Z3: contradictions between rules and
rules that can never trigger. F8 (or Ctrl+T) runs TLA+ with the real TLC model checker when Java
is available, and reads the result as a guard: which states each rule blocks, with blocked calls as
examples. Suggestions apply with Enter, the Agents tab replays recorded decisions against your edits
before anything changes, Ctrl+B binds agents, and Ctrl+L goes live; running guards switch on
their next call.
cslcore map --testEvery mapping is tested with case variants, unknown values, missing keys, wrong types and range
edges, and every derived check (path in scope, command allowed, destination allowed) with bypass
tricks: traversal, look-alike folders, chained and substituted commands, credentials and look-alike
hosts in URLs, and more, each built so the right answer is known. It works on your own mapper as it
is, keeps red-team findings as regression cases, and the classifiers in_scope, command_allowed
and destination_allowed pass every trick family. Guide: MAPPING.md.
cslcore watchThe live panel: agents with their mode and block rate, the decision stream, and rules ranked by how
often they would block, the ones to tune before switching to block. Switch an agent between log and
block (m), disable an agent or a single tool (kill switch), exempt an agent from a rule with a
recorded reason, or open the rule in the studio. l changes an agent's limits, w wires or
unwires it, a lists the calls waiting for your approval. Changes reach running agents on their next call,
without a restart, and every change is recorded in .csl/venom/audit.jsonl. The same controls are
on the command line: cslcore mode.
Press g for the live reach map: every decision flows over it as it happens, an ALLOW as teal
light from the agent toward what the call does, a WOULD BLOCK as a purple flash at the agent.
Policies are small, readable files. cslcore studio writes them with you, but they are plain text:
CONFIG {
ENFORCEMENT_MODE: BLOCK
CHECK_LOGICAL_CONSISTENCY: TRUE
}
DOMAIN PaymentsAgent {
VARIABLES {
tool: {"check_balance", "transfer_funds"}
amount: 0..100000
approval: {"YES", "NO"}
}
STATE_CONSTRAINT transfer_ceiling {
WHEN tool == "transfer_funds"
THEN amount <= 1000
}
STATE_CONSTRAINT approval_above_100 {
WHEN tool == "transfer_funds" AND amount > 100
THEN approval MUST BE "YES"
}
}cslcore verify payments.csl # compile and prove consistent with Z3
cslcore simulate payments.csl --input '{"tool": "transfer_funds", "amount": 500, "approval": "NO"}'
cslcore formal payments.csl # TLA+ model checking (real TLC, or --mock)
cslcore repl payments.csl # try inputs interactivelyFull grammar: syntax-spec.md.
The guard an agent uses at start; it follows its binding, mode and kill switches live:
from chimera_core.venom.observe import venom_guard
guard = venom_guard("payments-agent")
result = guard.verify("transfer_funds", {"amount": 500, "to_wallet": "w-03"}, {"approval": "YES"})
print(result.allowed)A policy on its own, without a workspace:
from chimera_core import RuntimeConfig, load_guard
guard = load_guard("payments.csl", config=RuntimeConfig(raise_on_block=False))
result = guard.verify({"tool": "transfer_funds", "amount": 5000, "approval": "YES"})
print(result.allowed, result.violated_rule_ids) # False ['transfer_ceiling']By default a blocked call raises ChimeraError, so an agent cannot carry on by ignoring a result.
Already have a guard (0.5.1)? One line adds decision logs, log mode and the live panel, and stays in block mode unless you switch it:
from chimera_core.venom.observe import observe
guard = observe(load_guard("policies/payments.csl"), agent="payments-agent")Where | How |
Claude Code |
|
Python tool functions |
|
LangChain / LangGraph |
|
Any Python agent |
|
Your AI assistant | MCP server: |
from chimera_core.plugins.langchain import guard_tools
safe_tools = guard_tools(tools=[search, transfer, delete], guard=guard,
inject={"user_role": "JUNIOR"}, tool_field="tool")Values in inject come from your system, not from the model, so it cannot override them.
The MCP server gives assistants (Claude Desktop, Cursor, VS Code) tools to verify, simulate, explain and scaffold policies, read what discovery found, and save drafts. Drafts are verified and never activated by the assistant; activation stays with you.
{
"mcpServers": {
"csl-core": { "command": "uv", "args": ["run", "--with", "csl-core[mcp]", "csl-core-mcp"] }
}
}Command | What it does |
| Guided first install, resumable |
| Read-only discovery; |
| The reach map, full screen: chains, dive into an agent, 3D globe |
| What each agent may do, in your own numbers; |
| Make |
| Put the guard in each agent's call path ( |
| Write, prove (Z3, TLA+), bind and go live, in the terminal |
| Live management panel |
| Generate mappings and run the mapping test ( |
| List, show, new, edit, extend, fix, verify, diff, activate |
| Log or block per agent, kill switches ( |
| Exemptions with a reason and an approver |
| Claude Code |
| Work on a single policy file |
Reference: cli-reference.md.
Deterministic enforcement. Prompt rules versus CSL-Core across four frontier models, 22 adversarial attacks (instruction override, role play, encoding tricks, multi-turn escalation, tool name spoofing) and 15 legitimate operations, run on 2026-02-18 with the model versions of that date:
Approach | Attacks blocked | Legitimate operations passed | Latency |
GPT-4.1, rules in the prompt | 10 / 22 | 15 / 15 | about 850 ms |
GPT-4o, rules in the prompt | 15 / 22 | 15 / 15 | about 620 ms |
Claude Sonnet 4, rules in the prompt | 19 / 22 | 15 / 15 | about 480 ms |
Gemini 2.0 Flash, rules in the prompt | 11 / 22 | 15 / 15 | about 410 ms |
CSL-Core | 22 / 22 | 15 / 15 | about 0.78 ms (median) |
The guard's own check, without the model call, is well under 0.1 ms; decision logging adds about 0.06 ms. Method and data: benchmarks/.
Compatibility you can check. Every release runs a contract suite generated from v0.5.1 (public API, CLI output, MCP tools, policy hashes, thousands of guard decisions) and the unmodified v0.5.1 test suite before anything else.
discover write and prove map run
┌──────────┐ ┌──────────────────────┐ ┌──────────────┐ ┌───────────────────┐
│ venom │ -> │ compiler .csl -> IR│ -> │ mapping test │ -> │ runtime guard │
│ 7 layers │ │ Z3 consistency │ │ bypass tricks│ │ fail-closed │
│ read-only│ │ TLA+ model checking│ │ regressions │ │ log / block, live │
└──────────┘ └──────────────────────┘ └──────────────┘ └───────────────────┘Verification happens before a policy runs; at runtime the guard only evaluates. A policy that fails Z3 does not compile, and a mapping that cannot read a value blocks the call instead of guessing.
Example | Domain | Shows |
AI agents | roles, PII protection, tool permissions | |
Finance | risk scoring, tiers, sanctions | |
Web3 | multi-sig, timelocks, emergency paths | |
Formal methods | TLA+ blocked states and examples |
python examples/run_examples.pyShipped: discovery of agents across seven layers, reach chains and the interactive reach map (3D globe, dive in, live decisions in watch), guided setup, policy studio with Z3 and TLA+, mapping tests with bypass tricks, live management panel with log and block modes, kill switches and exemptions, live policy reload, Claude Code and LangChain integrations, MCP server, upgrade path from 0.5.1.
Next: a hosted control plane for many machines (one view of every agent, central policy rollout, long audit retention), more framework integrations, and Linux packaging.
Issues and pull requests are welcome; start with CONTRIBUTING.md or a
good first issue.
Example policies and framework integrations are the most useful places to help.
Apache 2.0. Everything in this repository is free for any use, commercial, research or personal: the language, compiler, verifiers, discovery, setup, studio, mapping tests, live panel, CLI and MCP server. See LICENSE. A hosted control plane for running many machines from one place is offered separately.
Trademarks: Chimera Protocol and CSL are trademarks of Chimera Protocol. Apache 2.0 grants
rights to the code; trademarks are reserved.
Built by Chimera Protocol, originally for Project Chimera. For partnerships: aytug@chimera-protocol.com · Issues · Discussions
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 |
|---|---|---|---|
| variables | No | ||
| description | Yes | ||
| domain_name | 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 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 |
|---|---|---|---|
| dry_run | No | ||
| csl_content | Yes | ||
| context_json | Yes |
| 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 |
|---|---|---|---|
| timeout | No | ||
| use_mock | No | ||
| csl_content | Yes |
| 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.
One agent in detail: its tools with parameters and risk classes, triggers, guard status and the agent key to use in policies. No secrets, no prompt text.
Args: agent_id: agent id, name or key (from venom_inventory). workspace: Venom workspace folder.
| Name | Required | Description | Default |
|---|---|---|---|
| agent_id | Yes | ||
| workspace | 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 the full behavioral burden. It usefully discloses that the response contains no secrets and no prompt text, and implies a read-only inspection operation, but it does not cover permissions, side effects, rate limits, or error behavior.
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 front-loaded with the core purpose and then gives concise argument notes. It is appropriately sized for a two-parameter retrieval tool, with no redundant sentences, though the formatting is slightly awkward.
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 low complexity, output schema presence, and only two simple parameters, the description is nearly complete. It explains what the tool returns and how to supply each argument, leaving only sibling routing guidance unstated.
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%, so the description must compensate. It does so by explaining that agent_id accepts an id, name, or key from venom_inventory, and that workspace is a Venom workspace folder. This meaningfully expands on the bare schema titles.
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 states a specific resource and scope: 'One agent in detail' with its tools, parameters, risk classes, triggers, guard status and agent key. This clearly distinguishes it from the broader venom_inventory sibling, though it never names that sibling explicitly.
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?
Usage is implied by 'One agent in detail' and by noting agent_id comes 'from venom_inventory', which suggests a follow-up call after inventory. However, there is no explicit when-to-use guidance, no when-not-to-use conditions, and no named alternative for other agent-related needs.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Summary of the AI agents Venom discovered on this machine: kind, state, tool count, riskiest tool class, guard status, coverage and top findings. Redacted: no credential values, no prompt text.
Args: workspace: Venom workspace folder (default: CSL_VENOM_WORKSPACE or the server's folder).
| Name | Required | Description | Default |
|---|---|---|---|
| workspace | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It adds valuable behavioral context: the output is redacted (no credential values, no prompt text), which is important for an agent to know. However, it doesn't disclose whether there are side effects, read-only nature, rate limits, or permissions needed.
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 tightly structured with an overview paragraph and a clear Args section. Every sentence is informative, though the list of summary fields is a bit dense but still front-loaded with the purpose.
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 an output schema exists, the description need not detail return values, but it still enumerates them which is somewhat redundant. It omits usage context and behavioral traits like side effects or permissions, leaving gaps for an inventory tool in a policy/agent ecosystem.
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% and there is one optional parameter. The description does provide meaning for the workspace parameter, noting it defaults to CSL_VENOM_WORKSPACE or the server's folder. This compensates for the schema's lack of description, though only minimally with no format details.
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?
States a specific action (summarize/return inventory of discovered AI agents) with a clear enumeration of what the summary includes: kind, state, tool count, riskiest tool class, guard status, coverage, top findings. It's clear what the tool returns, though it doesn't explicitly differentiate from siblings like venom_agent or universe_info.
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 explicit when-to-use guidance or alternatives. A user must infer that this is the entry point for understanding a workspace's discovered agents versus using venom_agent or other siblings. No exclusions or conditions are stated.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Everything needed to draft or revise a policy for one agent: the active policy (or a deterministic starting draft on first install), its findings, vocabulary drift and the rules a valid draft must follow.
Args: agent_id: agent id, name or key. workspace: Venom workspace folder.
| Name | Required | Description | Default |
|---|---|---|---|
| agent_id | Yes | ||
| workspace | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the behavioral burden. It adds useful context about first-install behavior (deterministic starting draft) and that the payload includes findings and rules, but does not disclose read-only vs mutating semantics, permissions, or rate limits. Has an output schema, so return structure need not be described.
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?
Front-loaded with the tool's purpose in the first sentence, followed by a compact Args block. No filler, though the multi-line prose is slightly dense for a two-parameter read.
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?
For a context-fetch tool with an output schema, the description covers what is returned and both parameters. It lacks explicit usage routing among siblings, which given the many similarly named policy tools is the main remaining gap.
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%, so the description must compensate, and it does: it glosses both parameters ('agent id, name or key' and 'Venom workspace folder'), adding accepted formats beyond the bare schema types. It stops short of an example value or default behavior for workspace.
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?
States a clear purpose: retrieve everything needed to draft or revise a policy for one agent, enumerating the contents (active policy, findings, vocabulary drift, valid-draft rules). This is more specific than a name restatement, though it doesn't explicitly distinguish itself from siblings like explain_policy or scaffold_policy.
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?
Usage is implied by 'Everything needed to draft or revise a policy' and the notion of a deterministic starting draft on first install. However, there is no explicit when-to-use vs alternatives (e.g., scaffold_policy, explain_policy, verify_policy) and no when-not-to-use guidance.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Propose that an agent (scope "agent") or one tool (scope "tool") be exempted from guarding. Always recorded as proposed; only the operator can approve it in the CLI.
Args: agent: agent id (or "*" with scope "tool"). scope: "agent" or "tool". reason: why it can be trusted. tool: tool name when scope is "tool". workspace: Venom workspace folder.
| Name | Required | Description | Default |
|---|---|---|---|
| tool | No | ||
| agent | Yes | ||
| scope | Yes | ||
| reason | Yes | ||
| workspace | 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 the full burden and does well: it states that the action is always recorded as proposed and only the operator can approve it in the CLI, which is crucial behavioral context. It doesn't cover permissions or side effects beyond that, but the core workflow constraint is clear.
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 and front-loads the core purpose. The parameter list is terse and efficient, though the formatting (Args block) is slightly verbose for a short description.
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?
For a tool with 5 parameters, 0% schema coverage, and no annotations, the description is moderately complete: it explains the core mechanism (proposal only, operator approval) but leaves parameter details sparse. With an output schema present, return values are covered, but input semantics remain thin.
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%, so the description must compensate. It briefly lists the parameters (agent, scope, reason, tool, workspace) with minimal explanation, but doesn't clarify formats, constraints, or the special case of agent="*" with scope="tool" beyond a terse note. Most parameter semantics remain undocumented.
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 states a specific verb and resource: proposing an exemption for an agent or tool from guarding. It also hints at the two scopes and the approval restriction, making the purpose clear. It doesn't explicitly distinguish from sibling tools, but the proposal-specific nature is evident from the name and description.
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 when to use (when you believe an agent or tool should be exempt from guarding) but does not compare to alternatives or state when not to use it. Sibling tools like venom_policy_context or explain_policy might be relevant, but no routing guidance is given.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Verify a CSL draft (parse, validate, Z3) and, only if it passes, save it to the workspace's .csl/venom/drafts/. Never activates anything: the operator reviews and activates drafts with the cslcore CLI.
Args: agent_id: the agent the draft is for. csl_content: complete CSL policy source. note: one line explaining the draft (kept as a comment). workspace: Venom workspace folder.
| Name | Required | Description | Default |
|---|---|---|---|
| note | No | ||
| agent_id | Yes | ||
| workspace | No | ||
| 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 and does well: it discloses the gating verification pipeline (parse, validate, Z3), the target path, and the non-activation guarantee. It omits failure behavior (what happens on a failed verification) and whether it overwrites an existing draft.
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?
Front-loaded purpose followed by an Args block; every sentence earns its place except the note line, which slightly pads the count. Structure is easy to scan.
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?
An output schema exists, so return values need not be explained. The gaps are failure handling on verification failure and draft-overwrite semantics, which matter for a write tool with no annotations.
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 must document parameters, and it does: agent_id, csl_content, note, and workspace each get a one-line meaning. It does not cover defaults (note and workspace default to empty string) or the expected format/length constraints.
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 names a specific verb chain (verify then save) and a precise resource (CSL draft to .csl/venom/drafts/). It also explicitly states the boundary that separates it from activation, which no sibling tool covers. An agent can route confidently.
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?
Clear conditional usage: save only after parse/validate/Z3 pass, and never activate. It does not name sibling alternatives like verify_policy or simulate_policy, so the agent must infer when to prefer those over this tool.
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.6.7venom_agentvenom_inventoryvenom_policy_contextvenom_propose_exemptionvenom_save_draftv0.1.0explain_policyscaffold_policysimulate_policytla_verifyuniverse_infoverify_policyScored across 11 tools
Most tools are clearly distinct, especially the verification tools which have explicit guidance on when to use which (verify_policy vs tla_verify vs simulate_policy). The venom_* tools form a coherent workflow, though venom_inventory and venom_agent share the inspection space—inventory gives all agents, agent gives one—but the distinction is clear from descriptions. No major overlap or misselection risk.
Mixed naming conventions: venom_* tools use a clear prefix, but the rest are a mix of verb_noun (explain_policy, scaffold_policy), verb_verb (verify_policy, simulate_policy), and noun_verb (tla_verify, universe_info) patterns. While readable, there is no single consistent verb_noun pattern across the set.
11 tools are well-scoped for a CSL policy management and verification server. Each tool covers a distinct facet: inventory, agent inspection, policy context, drafting, exemptions, explanation, scaffolding, simulation, TLA+ verification, universe analysis, and Z3 verification. No tool feels redundant or missing.
The surface covers the full lifecycle of CSL policy work: inspection, drafting, verification, simulation, formal analysis, and exemption handling. One potential gap is direct activation or deployment of policies, but the descriptions explicitly state that activation is done via CLI by the operator, which aligns with the tool's design. No critical dead ends for the stated purpose.
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.
