I've been working on a TLA+ model checker in Rust and wanted to share it.

GitHub - fabracht/tla-rs
crates.io: Rust Package Registry

If you're not familiar with TLA+, it's a language for specifying concurrent and distributed systems. You describe your system's states and transitions, and a model checker explores every reachable state to make sure your invariants hold. The standard tool for this is TLC, which is written in Java.
It covers a practical subset of TLA+ and handles the specs I throw at it day to day.

Some things it can do beyond basic checking:

• Interactive TUI (-i) where you can step through states, evaluate expressions, trace variable changes
• --sweep to vary a parameter across values and compare results in a table
• --count-satisfying to measure what fraction of states satisfy a property, with per-depth breakdowns
• --scenario to drive exploration along specific paths using TLA+ expressions
• Liveness checking, symmetry reduction, DOT graph export
• Core library compiles to WASM

I'd love to hear feedback. Open an issue or create a discussion thread and I'll try to help as best I can

Cheers

1 post - 1 participant

Read full topic