Verify a CSL policy for logical consistency using Z3 formal verification.

Performs four-stage analysis:

1. Syntax validation (parser)

2. Semantic validation (scope, types, function whitelist)

3. Z3 logic verification (reachability, internal consistency, pairwise conflicts, policy-wide conflicts)

4. 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.

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.

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.

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").

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.

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.

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).

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.

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.

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.

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.