The recording of the Raft lecture is
now available (https://github.com/tlaplus/
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.