In order to incorporate TLA+ in LaTex sources it is best to download the JAR file for Standalone Tools.

• Main TLA+ Site (as of September 2019, version 1.60)
  • At the above site, TLA+ ToolBox/IDE (version 1.6) can be downloaded here.
  • The JAR file is obtainable here. This is referenced from Standalone Tools Overview.
  • Documentation for command line tools

I have done the following

alias tla2tex="java -cp /usr/local/tla-tools/tla2tools.jar tla2tex.TLA" 
alias tlaintex="java -cp /usr/local/tla-tools/tla2tools.jar tla2tex.TeX"

tla2tex model.tla 

This will produce tla.tex.

tlaintex model.tex 

where

% model.tex
\documentclass[12pt]{article}
\usepackage{tlatex}
\usepackage{color}
\definecolor{boxshade}{gray}{.9}\setboolean{shading}{true}
 
\begin{document}
\begin{tla}
  Action == /\ x'   = x - y
            /\ yy'  = 123
            /\ zzz' = zzz
\end{tla}
\end{document}

The style file tlatex.sty is available here.