Lamport TLA+ Course Lecture 1: Introduction to TLA+ (HD)

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/video/videos.html or the original page which is linked below.

Original Description: Explains what TLA+ is and why you might want to use it. It introduces the concept of a state machine.
Original Link: http://lamport.azurewebsites.net/video/intro.html
Corrections: http://lamport.azurewebsites.net/video/corrections.html#lecture1

Contents

0:00 - Intro
00:05 - Prologue
00:46 - What is TLA+?
02:46 - Abstraction
05:08 - What Engineers Say
09:41 - What Can TLA+ Check?
10:37 - The Basic Abstraction
12:50 - State Machines
14:25 - A Tiny Example
19:50 - Epilogue