Fonts
TLA+ widely uses the language of mathematics, and its syntax contains great deal of character sequences that represent mathematical symbols. So why not use those symbols directly when displaying specifications in the text editor?
There're two levels of visualization improvements:
Lots of fonts, especially designed for developers, have many ligatures that match TLA+ character sequences: Fira Code, Monoid, Hasklig, JetBrains Mono, PragmataPro to name a few.
Switch to one of such fonts, turn ligatures on (provide the "editor.fontLigatures": true VS Code setting), and you'll get many fancy symbols in your specs:
If you want go further, you can install the Conceal extension and configure substitutions to make your specifications look even closer to math texts:
More information about substitutions, including settings examples, can be found in the corresponding discussion.