Lamport TLA+ Course Lecture 7: Paxos Commit (HD)

Original Description: Specifies a real fault-tolerant algorithm for committing database transactions. It explains a few mathematical operations for constructing and combining sets.

Contents

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

[hoots]

Thanks for making these videos, very helpful