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
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
Videos of the talks are available