TLA+ is a formal specification language that uses ZFC set theory and temporal logic. It can be used to create formal models of systems and check various properties about them. You can read more about it here.
This guide is intended as a reference that people familiar with TLA+ can use to expand their knowledge of the language & tools, or quickly remind themselves of how some syntax or feature works. It focuses on model-checkable specs and features. It is not a TLA+ tutorial.
If you are interested in learning TLA+, you will be better served by other sources enumerated here.