[igornotarobot]

If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".

[mike_hock]

No, I just find the inconsistent syntax annoying, but it turns out most things have alternative Latex-style spellings. I just went by their examples.