How does Quint compare to TLA+ in terms of performance?

[ekexium]

Hi, I'm considering using Quint to model a somewhat complex system with a large state space.
I'm wondering what the performance difference is between Quint and TLA+.
I couldn't find recent benchmarks, and the apalache-tests repo looks stale.
Does compiling Quint to TLA+ and running it with TLC yield the same performance?
What are the best practices for complex Quint specifications? Is it better to rely on random simulation rather than full model checking?

[bugarela]

Hi! Nice to hear you are considering Quint!

Does compiling Quint to TLA+ and running it with TLC yield the same performance?

It should not make a significant difference, but we have not benchmarked this.

What are the best practices for complex Quint specifications? Is it better to rely on random simulation rather than full model checking?

For both simulation and model checking with TLC, the main best practice is to reduce the state space. For instance, you can avoid making a bunch of unnecessary transitions by using the "messaage soup" pattern explained here.
To use Apalache, you also need to take into consideration the complexity of expressions, since it will do constraint solving (while having to worry less about large state spaces when it comes to numbers, for instance, as it can solve equations without enumerating all values).

Realistically, if your state space is large, you will need to stick with simulations. In order to get more confidence from simulations, you need to convince yourself that it is covering enough of your state space. So you should write witnesses (properties that you expect to break at some point) and observe if they are actually breaking (or how frequently, by using the --witnesses arg). If you see that the simulator is finding those non-trivial scenarios, you can become more confident that it would also find violations to your actual properties.

The simulator with --backend=rust is fast and runs in parallel. No benchmarks done yet, but since a big bottleneck for TLC is storing states (and storing them in disk once your RAM fills up), and our simulator doesn't have to do that, I'm pretty confident that you'll be able to explore more of your state space with the rust simulator from Quint than with TLC.

[ekexium]

That's very helpful and informative. Thank you!

[pochenai]

The statement “if your state space is large, you will need to stick with simulations” may be somewhat misleading? In practice, model checking can still be effective even when the state space is moderately large.

As discussed in Igor Konnov’s article https://protocols-made-fun.com/testing/model-checking/2026/03/09/random-walks.html#quick-summary, modern model checking techniques often avoid naive enumeration of all states. Instead, they rely on optimizations such as symbolic representations, partial-order reduction, and SMT-based reasoning, which can prune large portions of the state space and focus only on relevant behaviors.

Because of these techniques, model checking can sometimes outperform random simulations when the system is “not too large,” especially if the bug lies in a rare corner case that simulations are unlikely to encounter.

[bugarela]

Of course! You took the "Realistically, " prefix of my sentence. In theory, these techniques help, although we don't have tools implementing partial order reduction for Quint/TLA+ yet. Apalache (symbolic, SMT-based) also helps in theory, which is why I mentioned it in my reply.

I was just trying to not over promise, based on practical industry-grade specifications we have written over the past years. Simulation will not catch all bugs, but it has provided us an immense amount of value, while model checking with existing tools often didn't fi the time budget.

I think this could change with more people paying attention to formal methods now, and maybe we'll get better tooling that is cabaple of using the amazing techniques that exist to bridge this gap and make model checking more accessible.