TLA⁺ in Practice and Theory

This 4-part series and a 40-minute video of a summary talk covers in detail the mathematical theory and design principles used in TLA⁺.

• Part 1: The Principles of TLA⁺

  TLA⁺ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.

• Part 2: The + in TLA⁺

  We explore the data logic of TLA⁺, the means by which TLA⁺ specifications describe a state of computation: its data structures. To do that, we first cover the basics of mathematical logic.

• Part 3: The (Temporal) Logic of Actions

  TLA, the Temporal Logic of Actions is the core of TLA⁺. It is a temporal logic that minimizes the use of temporal reasoning in favor of more ordinary mathematics. It is a general mathematical framework for describing and reasoning about algorithms and systems.

• Part 4: Order in TLA⁺

  We learn how to encapsulate and compose TLA⁺ specifications, of the precise mathematical definition of abstraction, and compare TLA⁺'s notion of abstraction with those of other formalisms. Plus some various cool stuff.

• Curry On Talk: The Practice and Theory of TLA⁺

  My Curry On talk about TLA⁺