Re: [Dr. TLA+ Series] Raft - Jin Li (Thursday, July 21st, 10-11:30am PDT)

The recording of the Raft lecture is now available (https://github.com/tlaplus/DrTLAPlus/blob/master/raft_lecture.md). Raft is a rather subtle algorithm, but Jin did a fantastic job explaining it and making the algorithm crystal clear.

The TLA+ part starts at 1 hour 5 minutes (01:05). The highlight of this part occurs at 01:15. When the audience asked whether certain information needs to be persisted, Jin modified the Raft TLA+ spec on the spot and demonstrated that TLC very quickly found an execution trace that causes invariant violation. This is a perfect example showcasing the power of specification and model checking.

Enjoy! J