CSL-Core
A formal constraint language for AI systems. Define causal rules, verify them with Z3, and make hallucinations structurally impossible.
Formal Verification
Every policy is verified by Z3 SMT solver for logical consistency before deployment. Dead constraints, conflicts, and unreachable rules are caught at compile time.
Causal Constraints
Define causal relationships between variables using WHEN/THEN rules. The constraint engine enforces state transitions that respect the causal structure of your domain.
Policy Simulation
Test policies against real-world inputs before deployment. Batch simulate thousands of scenarios and get ALLOWED/BLOCKED verdicts with full violation traces.
Zero Runtime Overhead
Policies compile to optimized intermediate representation. Guard evaluation adds microseconds, not milliseconds, to your pipeline.
Domain-Specific Types
Integer ranges, float ranges, string enums, and boolean types with static validation. Type mismatches caught at verification time, not runtime.
Python-First SDK
Native Python library with pip install. Verify, simulate, and guard in three lines of code. Integrates with any LLM framework.
Define. Verify. Guard.
Three steps from constraint definition to runtime enforcement.
Define
Write your constraints in CSL syntax
CONFIG {
version: "1.0"
enabled: true
dry_run: false
}
DOMAIN MedicalAgent {
VARIABLES {
diagnosis_confidence: 0.0..1.0
action: {"PRESCRIBE", "REFER", "INFORM"}
patient_age: 0..120
drug_interaction_risk: {"LOW", "MEDIUM", "HIGH"}
}
CONSTRAINTS {
WHEN diagnosis_confidence < 0.7
THEN action MUST NOT BE "PRESCRIBE"
WHEN patient_age < 18
AND drug_interaction_risk == "HIGH"
THEN action MUST BE "REFER"
ALWAYS True
THEN action MUST NOT BE "PRESCRIBE"
WHEN diagnosis_confidence < 0.3
}
}Verify
Z3 SMT solver checks for logical consistency
| Property | Value |
|---|---|
| Policy | medical-agent.csl |
| Domain | MedicalAgent |
| Constraints | 3 |
| Engine | Z3 SMT Solver 4.12 |
Guard
Runtime enforcement blocks unsafe actions
| Input | Value |
|---|---|
| diagnosis_confidence | 0.4 |
| action | "PRESCRIBE" |
| patient_age | 15 |
| drug_interaction_risk | "HIGH" |
| # | Rule | Condition | Status |
|---|---|---|---|
| 1 | diagnosis_confidence < 0.7 | action "PRESCRIBE" is prohibited | VIOLATED |
| 2 | patient_age < 18 AND risk == "HIGH" | action must be "REFER" | VIOLATED |
| Metric | Value |
|---|---|
| Total Simulations | 1 |
| Allowed | 0 |
| Blocked | 1 |
diagnosis_confidence (0.4) < 0.7 — action "PRESCRIBE" is prohibited. Patient age (15) < 18 AND drug_interaction_risk is "HIGH" — action must be "REFER".
diagnosis_confidence (0.9) > 0.7 — action "PRESCRIBE" is permitted. All 3 constraints satisfied. Action proceeds.