Video course by Leslie Lamport on TLA+

Leslie Lamport, the man behind TLA+/TLC, the formal modeling language we used to develop our RTOS kernel has started a series of video lectures on TLA+. If interested in a comprehensive and pragmatic approach to formal modelling, we can only recommend it.

The webpage with a discussion forum is here with the videos here.