CSL-Core Safety Enforcement

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.

Load CSL-Core syntax reference and common patterns for writing policies.

Hello World — simplest possible CSL policy (1 rule).

Age verification — multi-rule interaction with MUST BE / MUST NOT BE.

Banking transfer guard — tiered limits, sanctions, risk scoring.

AI agent tool guard — RBAC, DLP, hard bans with ALWAYS.

DAO treasury guard — arithmetic expressions, escalating approvals.