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.