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: Specifies a real fault-tolerant algorithm for committing database transactions. It explains a few mathematical operations for constructing and combining sets.
Original Link: http://lamport.azurewebsites.net/vide...
Corrections: http://lamport.azurewebsites.net/vide...

Contents

0:00 - Intro
00:41 - The Algorithm
03:11 - The Specification
14:03 - Checking the Spec
19:13 - Epilogue