Oh that's awesome. I first came across TLA+ (probably also through HN) about 6 months ago and recognized Leslie Lamport's name. The concept was very interesting but I had trouble getting to a good enough understanding of TLA+ to be able to use it. I'll look to see if I can find the associated NDC talk on youtube but his slides are also great. Thanks for sharing.
He does an incredible job conveying the ideas and intuition behind a lot of the terms and concepts for a given subject.
On a slight tangent, you might enjoy the slides from Scott on a different topic - model checking with TLA+ - from NDC Oslo this week:
https://www.slideshare.net/ScottWlaschin/tla-for-programmers...