Not exactly related, but there is the Apalache project: https://apalache.informal.systems/. This is a new model checker for TLA+ that translates a specification into an SMT-solvable constraint problem. One benefit of this is performance - SMT solvers are surprisingly fast, and they avoid exploring the state space directly as TLC does.
I think it's a very compelling idea though.
On Sunday, August 29, 2021 at 4:37:22 PM UTC-4 dmitry....@xxxxxxxxx wrote:
Are there tools or research projects, which use GPU to accelerate model checking of TLA+ specifications?