"Tackling Concurrency Bugs with TLA+" by Hillel Wayne
Strange Loop ConferenceYouTube ↗
Archive guide
Hillel Wayne's Strange Loop talk introducing TLA+ as a specification language for finding concurrency bugs in designs. It covers stalling, race conditions and dropped messages, with PlusCal examples.