Indeed it seems that the verification relies on Apalache, which is an alternate (symbolic) model checker for TLA.

TLA (well, TLA+) gives access to a richer specification language, as it allows e.g., to express liveness properties (informally defined as "something good happens at some point") as opposed to just safety ("nothing bad ever happens"). But the model checker does not use symbolic techniques so it may suffer on larger systems.

Personally I also find Quint to be way more readable/intuitive but your mileage may vary.

Thanks. More readable/intuitive is always welcome. I'll give it a try.

Two main things: alternative syntax and tooling

Some things that a programmer would take for granted are not available in TLA+ tooling, but are for Quint. The biggest examples: syntax and type checking in the IDE as you type, standard CLI with standard error reporting, LSP (Language Server Protocol) support (so you can use "Go To Definition" in your IDE).

In addition to that, Quint has a way to define tests (runs) and it makes it so it's easy to execute a specification, which is not normally possible in a natural way.

TLA+ has more advanced mathematical expressions that are not supported in Quint. This is on purpose. There are many things you can write in TLA+ but not in Quint, but those are the things that most people would only write by accident and be extremely confused by the results. The people who would write those knowing what they mean will probably like the Mathy syntax of TLA+ much better than Quint, so they should just use TLA+.

Thank you for your explanation.

https://FizzBee.io is not just a syntax transpiler, but a complete implementation. It uses starlark language (a Python variant) for specification. In addition to behavioral modeling like TLA+, Quint etc, it supports probabilistic and performance modeling. Generates state and sequence diagrams automatically.