Chimera-Protocol/csl-core

What's New

TLA⁺ Model Checking — cslcore formal

CSL-Core now ships a dual-engine formal verification stack:

| Engine | What it checks |
|--------|----------------|
| Z3 | Logical consistenc: Contradictions, unsatisfiable constraints |
| TLA⁺ / TLC | Temporal safety: Exhaustive state-space exploration, counterexample traces |

cslcore formal policy.csl

Runs the official TLC model checker (java -jar tla2tools.jar) against your policy. TLC's own version string, process ID, and worker count are surfaced in the terminal — cryptographic proof that real model checking ran, not simulation.

Highlights

• Predicate abstraction — large numeric ranges (e.g. 0..100000) automatically reduced to a finite abstract domain while preserving soundness
• Counterexample traces — exact state that violates your invariant, with root-cause analysis and 3 concrete fix suggestions
• Auto-download — tla2tools.jar fetched automatically on first use (~4MB), no manual setup
• Graceful fallback — if Java is unavailable, falls back to Python BFS model checker; banner clearly labels which engine ran
• ENABLE_FORMAL_VERIFICATION: TRUE — opt-in flag triggers TLA⁺ at compile time

New Files

• chimera_core/engines/tla_engine/ — full TLA⁺ engine (spec builder, TLC runner, verifier, animations, suggestion engine)
• examples/tla_demo.csl — all properties hold
• examples/tla_demo_violation.csl — counterexample trace demo
• tests/test_tla_real_integration.py — 49 integration tests

Install

pip install csl-core==0.4.0