TLA+ with Leslie Lamport

TLA+ is a formal specification language. TLA+ is used to design, model, and verify concurrent systems. TLA+ allows a user to describe a system formally with simple, precise mathematics.

TLA+ was designed by Leslie Lamport, a computer scientist and Turing Award winner. Leslie joins the show to talk about the purpose of TLA+. Since its creation in 1999, TLA+ has been used to discover bugs in systems such as Amazon S3, DynamoDB, Xbox, and Cosmos DB.

“TLA” stands for “temporal logic of actions”, a logical system that can be used to describe the behaviours of concurrent systems.

This podcast is meant as a brief introduction of TLA+. To go deeper, check out the TLA+ website and the TLA+ video course (note: these videos are highly entertaining because of Leslie’s dry, unpredictable sense of humor).