If you liked that book, Software Abstractions is the Alloy version. It has some great examples and exercises. Easily translatable to TLA+. And I think the lessons demonstrate well why writing specifications is helpful.

From there, if you’ve digested those books then get to writing some specifications. Join the mailing lists or find a group on discord or slack or something. Try modelling an elevator. Make sure that every person that calls the elevator eventually arrives at their requested floor. Pick a favourite async library and see if you can model its structures and functionality. The important thing is to exercise that muscle and make mistakes.

Thanks!

Just for completeness apparently Alloy is at version 6 now (http://alloytools.org/alloy6.html) and the book is based on version 4 (http://alloytools.org/book.html). There's another resource linked on the site: https://haslab.github.io/formal-software-design/