Lamport’s book and or Hillel Wayne’s are both good. State machines as a specification language has always been pretty approachable and also relatively deep. If you want to get in to proof assistants Software Foundations is great and the delta to understanding Lean from Rocq is pretty small.

https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/