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 sp

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.