https://learntla.com/

|||

Learn TLA+

 

 

Quick search

[                    ] [Go]
  * Intro
  * FAQ
  * What's New
  * Conceptual Overview

TLA+

  * Core
  * Topics

Examples

  * Operators
  * PlusCal Specs

Reference

  * Glossary
  * Standard Modules
  * Other Resources

  * Index

Note

Welcome to Learn TLA+! This is still a work in progress, please see
What's New for updates and please raise any questions or concerns at
the github repo. I'd love to hear your feedback!

(In the meantime, you can find the old version at old.learntla.com.)

Learn TLA+P

Most software flaws come from one of two places. A code bug is when
the code doesn't match our design-- for example, an off-by-one error,
or a null dereference. We have lots of techniques for finding code
bugs. But what about design flaws? When it comes to bugs in our
designs, we're just taught to "think about it really hard".

TLA+ is a "formal specification language", a means of designing
systems that lets you directly test those designs. Developed by the
Turing award-winner Leslie Lamport, TLA+ has been endorsed by
companies like AWS, Microsoft, and Crowdstrike. TLA+ doesn't replace
our engineering skill but augments it. With TLA+ we can design
systems faster and more confidently. Check out the Conceptual
Overview to see an example of this in practice.

About this guideP

This is a free online resource for learning TLA+. To help both
beginners and experienced users, the guide is divided into three
parts:

  * The Core: a linear introduction to all of the TLA+ language. It
    starts with basic operators and gradually progresses all the way
    to advanced topics. The core is intended to be read linearly:
    people new to TLA+ should start with the conceptual overview and
    then work forward from there. People comfortable with TLA+ should
    skim until they find new material.

  * Topics: "Optional" advanced material. Any individual lesson will
    be useful to many but not all TLA+ users. Unlike the core, these
    are designed to be mostly independent of each other. If topics
    have dependencies on other topics, I will call them out.

  * Examples: Applications of TLA+ to specs, showing both how to
    write and understand specs.

This guide is still under development, check What's New to see most
recent updates and the roadmap to see what I'm currently working on.

About MeP

I'm Hillel. I'm part of the TLA+ foundation and the author of the
book Practical TLA+. I wrote this because I want TLA+ to be as
accessible as possible and didn't like that my book cost money. I
have a blog, a twitter, and a weekly newsletter.

(Full disclosure, I'm also a professional TLA+ consultant and <plug>
run workshops</plug>.)

<Page contents

>Page contents:

  * Learn TLA+
      + About this guide
      + About Me

FAQ>
(c) Copyright 2022, Hillel Wayne. Created using Sphinx 4.4.0.

Styled using the Piccolo Theme