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).


Transcript provided by We Edit Podcasts. Software Engineering Daily listeners can go to to get 20% off the first two months of audio editing and transcription services. Thanks to We Edit Podcasts for partnering with SE Daily. Please click here to view this show’s transcript.

Software Daily

Software Daily

Subscribe to Software Daily, a curated newsletter featuring the best and newest from the software engineering community.