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.