[colanderman]

Interesting, the notation used in that paper presages the notation used by TLA⁺² [1]. I actually have written up an exposition of TLA⁺² proof steps using sequent calculus notation [2] with the intention of writing a proof visualizer for it.

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...

[2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...