TLA+ | The way to specify

Learning

TLA+

This is the section to go to if you are new to TLA+ and want to find out what it’s all about–particularly its How to Start section.

PlusCal

PlusCal is a language for writing algorithms that is based on TLA+; but it’s possible to start with PlusCal and learn the TLA+ that you need to use it as you go along.

Examples

This section has examples of how TLA+ and PlusCal are used. It contains the examples from the TLA+ book and others, created both by Leslie Lamport and other people.