About TLA+

TLA+ is the specification language of the Temporal Logic of Actions (TLA), designed by Leslie Lamport. TLA is a logic which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent systems.

TLA+ is a mathematical language (not a programming language) and presents features which may be unfamiliar to some, such as

• Indentation significant syntax
• Lack of bracketing
• A rich set of operator symbols available to define in/pre/ or postfix operators.

It's also not context-free.
TLA+'s fundamental theories include set theory, first order logic and TLA. All relevant operators are considered builtin. The tool "knows'' a number of other operator symbols, but will require that a definition be provided ro resolve correctly.
Practically, this means that a specification with, say, arithmetic operators, will be parsed correctly, but an error might be reported if there is no definition for +.
The set of user-definable in/pre/postfix operators, along with their precedence and associativy, is built in, as well as the definition of "core'' operators. It is possible that some tools would require changes or additions to this list and support mechanisms exist for this purpose.