exit_code: 0
---

╭──────────────────────────────────────────────────────────────────────────────────────────╮
│ CSL-Core  v<VERSION>                                                                         │
│ Deterministic Safety Layer for Probabilistic AI Systems                                  │
╰──────────────────────────────────────────────────────────────────────────────────────────╯

╭──────────────────────────────────────────────────────────────────────────────────────────╮
│ Verifying policy                                                                         │
│ policies/examples__tla_demo.csl                                                          │
╰──────────────────────────────────────────────────────────────────────────────────────────╯

⚙️  Compiling Domain: AIAgentSafetyDemo
   • Validating Syntax... ✅ OK
   ├── Verifying Logic Model (Z3 Engine)... ✅ Mathematically Consistent
   ├── Running TLA⁺ Model Checker (Temporal Logic of Actions)…

╔══════════════════════════════════════════════════════════════════════════════════════════════════╗
║                                 TLA⁺ FORMAL VERIFICATION ENGINE                                  ║
║                    Chimera Specification Language · Temporal Logic of Actions                    ║
║                                                                                                  ║
║             ⚙  BFS Mock Engine  ·  Python State-Space Explorer  ·  (TLC unavailable)             ║
╚══════════════════════════════════════════════════════════════════════════════════════════════════╝

╭──────────────────────────────────────────────────────────────────────────────────────────────────╮
│   ◉  Constructing Universe: "AIAgentSafetyDemo"                                                  │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯

                     Universe Variables                     
                                                            
  Variable      Domain                         Cardinality  
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 
  agent_tier    {"STANDARD", "PREMIUM"}                  2  
  task_type     {"READ", "WRITE", "ANALYZE"}             3  
  environment   {"dev", "staging"}                       2  
  approved      BOOLEAN                                  2  
  risk_score    0..5                                     6  
                                                            

╭──────────────────────────────────────────────────────────────────────────────────────────────────╮
│   ◉  Expanding State Space  (BFS / Breadth-First Search)                                         │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 144 / 144 states depth=48 frontier=0 <T>
  └─ 144 states reachable · depth 48 · universe fully mapped

╭──────────────────────────────────────────────────────────────────────────────────────────────────╮
│   ◉  Verifying Temporal Properties  □(WHEN … THEN …)                                             │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯

 ├─ □(no_destructive_ops) ✅ HOLDS [12 states <T>]

 ├─ □(no_production_access) ✅ HOLDS [12 states <T>]

 ├─ □(bounded_risk) ✅ HOLDS [12 states <T>]

╭──────────────────────────────────────────────────────────────────────────────────────────────────╮
│   ◉  Generating Proof Certificate (SHA-256 signed)                                               │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯

  └─ Proof hash: 5a3a9196488fdaadda04f19cdde1317c… ✅


╔════════════════════════ TLA⁺ VERIFICATION COMPLETE — ALL PROPERTIES HOLD ════════════════════════╗
║                                                                                                  ║
║    ✅  Domain     : AIAgentSafetyDemo                                                            ║
║    ⬡  States     : 144                                                                           ║
║ ⏱ Total time : <T> ║
║    🔐 Proof hash : 5a3a9196488fdaad…                                                             ║
║                                                                                                  ║
╚══════════════════════════════════════════════════════════════════════════════════════════════════╝

   └── ✅ TLA⁺ Verification passed — all temporal properties hold
   • Generating IR... ✅ OK
                                  Compiled Policy Metadata                                  
                                                                                            
  Key                            Value                                                      
 ────────────────────────────────────────────────────────────────────────────────────────── 
  Domain                         AIAgentSafetyDemo                                          
  Policy                         AIAgentSafetyDemo                                          
  Policy Hash                    9db4a2b55896653b7d3aa9cdf8f9a8d979cf3f0796c160350c1b9dca…  
  Engine Version                 <VERSION>                                                      
                                                                                            
╭──────────────────────────────────────────────────────────────────────────────────────────╮
│ Verification passed                                                                      │
│ No logical contradictions found (given CSL-Core analysis scope).                         │
╰──────────────────────────────────────────────────────────────────────────────────────────╯

                 ✨ If you find CSL useful, please consider starring us on GitHub:                  
                           https://github.com/chimera-protocol/csl-core                             

