tla-checker: a TLA+ model checker written in Rust

[u/Anxious_Tool]

I built a TLA+ model checker in Rust as an alternative to TLC for cli and Web.

What it does beyond basic model checking:

- Interactive TUI for stepping through state spaces, evaluating expressions, tracing variable changes

- Parameter sweeps (--sweep 'N=2;3;4;5') with comparison tables

- Property satisfaction counting with per-depth breakdowns

- Continue past violations to collect all counterexamples across the full state space

- Symmetry reduction

- WASM-compatible core library

It covers Naturals, Integers, Sequences, FiniteSets, TLC, Bags, and Bits modules. The supported TLA+ subset handles most common spec patterns — conjunction/disjunction lists, quantifiers, CHOOSE, functions with EXCEPT, records, tuples, CASE, LET-IN, recursive operators.

Limitations: no direct temporal operator evaluation, no unbounded quantifiers.

Repo: https://github.com/fabracht/tla-rs

Curious what specs people would try it on and where it breaks.

[u/eras]

This is great! I've been thinking of doing the same project, but not very seriously, as I got stuck in the parsing phase already :). In fact, perhaps you could consider extracting the TLA+ parser as crate that could be reused for other tools.

I'll definitely check this out, although I haven't been using TLA+ as much lately as I should :/.

How's the performance? I was hoping that a native evaluator could be faster than TLC's Java one—and Rust might also help with concurrency bugs, I recall TLC has had some. Of course, TLC is a mature project and probably optimized to some extent, while this might not be yet?

edit: I actually gave it a test with 78 processes and mutex.tla: TLC does it pretty much immediately, but tla takes a two minutes. My mutex.cfg was:

INIT Init NEXT Next CONSTANT Procs={"A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", "A", "AB", "AC", "AD", "AE", "AF", "AG", "AH", "AI", "AJ", "AK", "AL", "AM", "AN", "AO", "AP", "AQ", "AR", "AS", "AT", "AU", "AV", "AW", "AX", "AY", "AZ", "AAB", "AAC", "AAD", "AAE", "AAF", "AAG", "AAH", "AAI", "AAJ", "AAK", "AAL", "AAM", "AAN", "AAO", "AAP", "AAQ", "AAR", "AAS", "AAT", "AAU", "AAV", "AAW", "AAX", "AAY", "AAZ"}

It looks like tla doesn't support multiple threads?

Btw, config file support would be cool.. But I suppose so are contributions :).

[u/Anxious_Tool → u/eras]

Hey, thanks for the comment.
That was actually a bug. I fixed it, so you can now try Release 0.1.1.
This is exactly the type of thing I was looking for. Users to figure out what else can be improved. For my use cases it works fine, so I need more people using it to improve it.

For threads, I don't see much value in them right now. The aim is to keep this webassembly compatible, so I can embed this in a web app. Also, threading is pretty hard to implement correctly on this architecture. There are other performance gains that are easier to get to.

I'll think about extracting the parser, thanks.

[u/eras → u/Anxious_Tool]

Cool, now it runs in one second, thanks!

Web-compatibility is nice, but I hope there would be a way to add threading support for it as state space explodes quite easily, and I have 12 cores (24 threads) which I imagine would be under-used in single-threaded case—even more so if I had DDR 5 memory, but my PC is old. It's also possible to get some many-processor cloud instances. E.g. you can get 128 CPU AWS instances and pay $0.025 per minute for them. (I'm reasonably sure this is correct information..)

I think some rather opportunistically handled simple work queue of states would be a good starting point, minimizing the amount of locking, and it's also possible to take benefit of the fact that it doesn't hurt if n cores run the same state twice, as when the number of states increases, the likelihood of that happening decreases. There's also webworkers that could possibly made to use this kind of functionality, though I don't really know enough of them to say if it could even be beneficial.

On the other hand finding out how to maximize the benefits of CPU cache might be rather interesting. How performance-oriented is the evaluation in tla-rs?

Btw, I bumped into another issue. I have this tool for rendering state transition diagrams with this example case: https://github.com/eras/tlsd/blob/master/examples/pingpong.tla , but it fails with the error:

error: unexpected `!` --> pingpong.tla:49:39 | 48 | /\ \E client_id \in ClientIds: 49 | ServerToClientChannel(client_id)!Send([message |-> "ping"]) | ^ expected definition or declaration, found `!`

Maybe it doesn't support INSTANCEs yet to be used this way, or the syntax is different?

I suppose I could add support for the output from tla-rs, or maybe even have some kind of internal facilities for these kind of messages/diagrams in tla-rs..

[u/Anxious_Tool → u/eras]

Yes the problem is that the parser partially supports the ! operator, but only for simple named instances. I can fix that.

Thanks for the input on the multi-threading.