IMPORTANT NOTE!: This is a mirror of Lamport's TLA+ lecture videos with some chapter markers in the video description from Lamport's site for ease of viewing on mobile devices, or other platforms and connection setups where YouTube is the most optimal "format". For the original files, resources, errata, and more, please visit http://lamport.azurewebsites.net/vide... or the original page which is linked below.

Original Description: Describes resources for learning about TLA+.Explains how to download the Toolbox and shows how to use it to open a spec, view the pretty-printed version, and run TLC on it.
Original Link: http://lamport.azurewebsites.net/vide...
Corrections: http://lamport.azurewebsites.net/vide...

Contents

0:00 - Intro
00:03 - Prologue
00:25 - TLA+ Resources
01:43 - Downloading the Toolbox
02:47 - Creating a Spec
04:36 - The Pretty-Printer
05:15 - Running TLC
08:36 - The TLA+ Proof System
09:09 - The Unicode Option
09:58 - Help!
10:40 - Epilogue