Quint [1] is a specification language heavily based on TLA+ but without the mathy syntax people have issues with, and without inheriting the tool problems of a language that was never designed to be "code" (i.e. Quint has types and good IDE support).<p>Quint also has the concept of a run, where users can guide the "searcher" to a specific set of executions, so it works really well as a BF/DF* searcher, which is it's focus (it doesn't support refinement or proofs, at least for now).<p>So yeah, if you are curious for a language that supersedes TLA+, you should definitely give Quint a try :)<p>* BF through model checking, DF through bounded random simulation<p>[1]: <a href="https://quint-lang.org/" rel="nofollow">https://quint-lang.org/</a>