Lightning talk I (@berenguel) gave at Scala Exchange on December 2018 to give a quick overview of TLA+ and PlusCal and how they can be used to model systems we use as Scala developers.
You can find the slides here. I recommend you check the version with presenter notes here. You can watch the live recording here. You can play a bit with TLA+ online (specifically with the examples used in this presentation) via the Binder link above, thanks to the work of Stas Kelvich to provide a Jupyter kernel for TLA+.
Sadly the PDF does not show animated gifs or videos, you can either check what they are in the images folder or watch the video.
This presentation is formatted in Markdown and prepared to be used with Deckset. The drawings were done on an iPad Pro using Procreate. Here only the final PDF and the source Markdown is available. Sadly animated gifs and video are just static images in the PDF.