My spare time is kind of... weird. They were related to concurrency in an actor system, I validated a design and implementation (can’t share much more). I recommend checking Hillel’s blog as suggested, he has excellent examples (and his book is a good starting point for TLA+ and Pluscal as well)