FizzBee is likely a good place to start, but since I have never really used it I'm afraid I can't recommend good resources for it.

------

If you're just getting started, I recommend checking out my former advisor's book: https://www.amazon.com/Software-Engineering-Mathematics-Sei/...

I found this book to be fairly easy to read through, and gives you a rundown of a lot of the notation and concepts that pretty much all formal methods systems require.

------

TLA+ is a decent enough language. I recommend going through Lamport's video series on it to start: https://lamport.azurewebsites.net/tla/learning.html

I don't know what aspect of Formal Methods that you want to focus on; most of what I've done is with distributed systems stuff, but TLA+ can and has been used for low level things like circuit modeling. I can't tell you where to learn about that.

I think Hillel Wayne's learntla website is pretty good to get a few more practical examples: https://learntla.com/. I actually thought his Practical TLA+ book was a bit better for that though: https://www.amazon.com/Practical-TLA-Planning-Driven-Develop...

Both of those resources are more PlusCal focused. PlusCal is a C/Pascal-like language that compiles to "raw" TLA+. A lot of people like it more, I go back and forth.

If you care more about the more theoretical aspects of TLA+, Ron Pressler's "TLA+ in Practice and Theory" blog series is great: https://pron.github.io/tlaplus

Additionally, I recommend looking for the papers by Stefan Merz. Here's a good one to start, but he has a bunch: https://members.loria.fr/Stephan.Merz/papers/tla+logic.pdf

------

If your goal is to model concurrent systems, getting an understanding of CSP is worth doing. I liked Roscoe's book on it: https://link.springer.com/book/10.1007/978-1-84882-258-0

If you go deep into that, I recommend looking at the extension "tock-CSP" that adds timing semantics.

-------

If you're interested in the most theoretical aspects of formal methods, the only one I've done with any kind of intimate detail is Isabelle.

Isabelle is much more of a "math proof" thing than a "computer science" proof thing, but there are plenty of computer science things for it too. If you want to get started with the Isabelle/HOL language, the Concrete Semantics book is the normal recommended starting point: http://concrete-semantics.org/

------

This is mostly my history, there are many other paths but I can't really speak to those with any confidence. Hope this helped!

ETA:

Just to add, while I did go to school later for formal methods, I actually started learning this stuff while I was still a dropout from my undergrad. I eventually got my bachelors and masters and then entered a PhD program, but for TLA+ in particular I was learning it without any completed education, so this stuff is definitely approachable even without a ton of letters after your name.