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: Commitment, in marriage and database transactions, is specified. You also learn how to use mathematical functions in specifications.
Original Link: http://lamport.azurewebsites.net/vide...
Corrections: http://lamport.azurewebsites.net/vide...

Contents

0:00 - Intro
00:02 - Prologue
00:53 - Weddings
04:14 - Transaction Commit
05:15 - The TLA+ Spec
18:14 - Checking the Spec
22:06 - A Parsing Note
22:58 - Comments
24:06 - Epilogue