I've been trying to get into formal specification & verification too, but with Z notation (which is specifically for specification) instead, together with a couple of different theorem-provers. It's for a pet project to help me learn, so not something I would be using for serious work (not right away at least), but I find the Z notation quite readable and there is quite a bit of support and free tooling for it available online. Being quite new to formal methods, I think TLA+ would be overkill for learning.