Using TLA+ for fun and profit in the development of ElasticSearch [video]

TLA+ is less a programming language and more a systems modeling language. It's like writing a mathematical proof for your system where you describe each action the system takes, the invariants to describe "correctness" of the system and its state, and the TLA checker runs some kind of analysis of every possible state described by your model and that the invariants still hold true for all possible states. To me, it's like running a unit test in parallel where all possible inputs are provided concurrently.

I'm not an expert on it, but I've worked with it some to verify distributed systems at a FAANG company (with the oversight of real experts)--so it does get used there!

TLA+ allows you to encode your system as a state machine, define invariants that must always be true, and the checker will explore your state machine and verify that the invariants are always true.

An example would be encoding a distributed locking system, with an invariant saying "no lock is owned by more than 1 node at a time". You would encode all of the locking and unlocking behavior in your state machine, and then the checker would verify it.

You can also use the model checker to, via brute force, find a sequence of states that result in a desired outcome (which is expressed as a set of conditions called an “invariant”). For example, steps to solve the tower of honoi or the Die Hard 3 jug problems.

TLA+ is a formal language for specifying a state machine and properties it may satisfy (e.g. eventually/never reaches a given state). Since many systems, from simple algorithms to entire distributed systems, can be thought of as state machines, TLA+ serves as a useful formal design language for documenting them and the expected behavior they should follow. On top of this, the TLA+ ecosystem comes with tools to verify that your proposed design indeed satisfies the properties you have written, increasing confidence that your design is sound and doesn't have weird corner cases you haven't thought about.

I can recommend Hillel Wayne's book "Practical TLA+". It helped me understand scenarios where TLA+ specifications and the modelling approach would be essential in discovering bugs before writing any code. (Still waiting to put my fledgling TLA+ knowledge to some actual application though, as I'm currently working on some graphics stuff with nothing distributed about it...)

Wayne also has a great blog: https://www.hillelwayne.com

Btw, not all great technology finds adoption at the FAANGs. At least Facebook and Google tend to be quite insular: they certainly don't frown on open source, but it must be something that can be assimilated into the worldview of hulking monorepos, company IDEs and tools teams.

To put it another way: if Facebook/Google are giant Borg cubes, then TLA+ is a clever little Vulcan ship applying pure logic to stay in the game.

Leslie Lamport, creator of TLA+, has described it as blueprints for your system. You can describe your system at any level of detail, and state assertions/assumptions about it. You can then use tools to check if your assertions are correct.

it's kind of a proof assistant, not really a programming language, focusing on finding gaps in invariants during state transitions.

i suggest spending a few hours with author's own video course: https://lamport.azurewebsites.net/video/videos.html

it is generally useful, what it doesn't do is emit working prototypes.

TLA+ is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems

https://en.m.wikipedia.org/wiki/TLA%2B