Leslie Lamport

Last modified on 23 August 2019

Videos of Paxos Lectures

Videos of two lectures describing the Paxos consensus algorithm with TLA+ are available here.  In addition to explaining the algorithm, they provide a crash course on TLA+.

TLA+ Conference at Strange Loop 2019

The conference will take place in St. Louis, Missouri, USA, on 15 September 2019.  See this announcement.

Checking Inductive Invariance with TLC

If you've written rigorous correctness proofs of concurrent algorithms described in TLA+, then you know that the key to the proof is an inductive invariant.  Finding the right inductive invariant is hard.  It should be made easier by new features added to TLC for checking that a formula is an inductive invariant.  What an inductive invariant is and how to use TLC to check if a formula is one are described in this document.

2018 TLA+ Community Meeting

A TLA+ community meeting was held in Oxford, England on 18 July 2018.  The program, containing links to papers or extended abstracts and slides for the talks, can be found here.  Videos of the talks are available here.