
------
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.
I also think his book "Software Engineering Mathematics" [2] is an extremely approachable book for any engineer who wants to learn a bit more theory.
As I said, my dropped PhD is not a failure in any capacity from my advisors or the school, mostly just life juggling stuff.
[1] I don't know why exactly, but of all the places I've been, York has the highest percentage of "genuinely nice" people. It's one of my favorite spots in the UK as a result.
[2] https://a.co/d/02M25LcY, not a referral link.
The Mathematical Notation is THE universal language of Logic, Set Theory, Functions etc. which are the mathematical underpinnings of Computer Science and Programming. This is what all Engineers need to be familiar with. Programming languages are incidental in this case and are merely used for syntactic expressions of Mathematical Concepts. This is as it should be and the reason Leslie Lamport (the inventor of TLA+) settled on this specific notation. Please see his interviews/videos on Youtube for more details.
In my own case i started by grasping/studying the basics from the following books;
* Software Engineering Mathematics by Woodcock and Loomes.
* Understanding Formal Methods by Monin.
* Introductory Logic and Sets for Computer Scientists by Nimal Nissanke.
* Mathematical Notation: A Guide for Engineers and Scientists by Scheinerman.
This allowed me to start studying Specifying Systems by Leslie Lamport which is the main book for TLA+.
PS: User "pron" to whom you replied to has a nice 4-part series on TLA+ which i have linked to in another post in this thread. He really knows this subject :-)
The Redditor is talking about a specific trap that some people who've been told from a young age that they're smart fall in to, at different ages. The trap involves - mostly - having not been challenged previously, and not knowing how to work through things that don't come easily.
When I was a kid, I spent 6 years at a school in Barbados, and some time at a school in Thailand, where I was unambiguously the smartest kid in the class, with the top grades, always. Then at 10 I went to the UK's largest prep school. I was behind in Latin, French, and a bunch of other subjects - especially those which required any rote learning (which I hadn't come across up to that point).
The transition to a school with /much/ better teaching saw me become a distinctly mediocre student almost straight away - faced with challenges, and faced with not being able to simply smart my way to the top of the class, I started rejecting work wholesale - something that stayed with me throughout the rest of my formal education, and led to me getting some truly shitty A-Level grades, to the disgust of teachers who saw much greater potential there.
Hard work and talent are both important, and so is the ability to encounter and handle challenge. If you grew up in an environment where you were coasting at the top, the first time you encounter serious challenge you might well fall apart.
I've recently started an MSc at what Americans would call an Ivy-League university (having talked my way without an undegrad degree), and the first module I'm working with is "Software Engineering Mathematics". Working through the chapters of the book I have consistently had real trouble getting to grips with the material. I want it to just fit in straight away - and I just want to understand it - and it doesn't, and that's a constant challenge.
Being a little older, and a little more mature, I'm throwing everything I have against it now, and seeing real dividends for perseverance. But every day is a struggle of fighting against the part of me that doesn't know how to deal with challenge, and I put that down to the sudden transition from coasting to the top to sudden massive challenge, and having not dealt well with it at the time - which it sounds like the very very original poster was also struggling with.