Alloy is a model checker that has a GUI for exploring models. It's more focused on exploring structures. Their site links to a book, Software Abstractions, that will teach you a lot of concepts without needing a strong, mathematical background.
If focus is programming (esp low-level), SPARK Ada lets programmers annotate code with the expected behavior before that's fed into provers that confirm or refute the code operates that way in all situations. Barnes and Barnes wrote a nice book teaching both it and Praxis' Correct-by-Construction method for software development:
Many people don't make it through the stuff teaching formal proof in Coq and so on. It's really hard with few gains along the way. TLA+, SPIN, Alloy, and SPARK Ada are much more accessible with a higher work-to-reward ratio. Those easier results might justify further investment in learning the hard stuff.
Those wondering about how formal methods are used in a lot of situations might like our list on Lobsters. We have a number of professionals and enthusiasts there who stay posting both historically significant and cutting-edge work.
And with SPARK if you want to dive into manual proof of a property (usually because SPARK & Why3 and all the SMT solvers can't manage and you don't have some appropriate lemmas) with Coq or Isabelle.
Not the best way to learn manual proof, but I've seen it used very efficiently.
But then if course you're faced with the difficulty of increasing automation : the more you automate, the more it is difficult to have the 'muscle memory' (and lower cognitive load) that you get when flexing the manual proof often...
Even that is getting automation as I long ago predicted. I think the SPARK-type proofs will be easier to automate this way, too, since they're more mechanical.
If you like distributed systems, Hillel Wayne's book on TLA+ will let you see how model checking can easily spot errors that are hard to test for:
https://www.apress.com/gp/book/9781484238288
Spin has been used in similar ways for a long time:
https://spinroot.com/
Alloy is a model checker that has a GUI for exploring models. It's more focused on exploring structures. Their site links to a book, Software Abstractions, that will teach you a lot of concepts without needing a strong, mathematical background.
https://alloytools.org/about.html
Pamela Zave used both Spin and Alloy to find errors in real-world protocols:
http://www.pamelazave.com/compare.html
If focus is programming (esp low-level), SPARK Ada lets programmers annotate code with the expected behavior before that's fed into provers that confirm or refute the code operates that way in all situations. Barnes and Barnes wrote a nice book teaching both it and Praxis' Correct-by-Construction method for software development:
https://www.betterworldbooks.com/product/detail/High-Integri...
Many people don't make it through the stuff teaching formal proof in Coq and so on. It's really hard with few gains along the way. TLA+, SPIN, Alloy, and SPARK Ada are much more accessible with a higher work-to-reward ratio. Those easier results might justify further investment in learning the hard stuff.
Those wondering about how formal methods are used in a lot of situations might like our list on Lobsters. We have a number of professionals and enthusiasts there who stay posting both historically significant and cutting-edge work.
https://lobste.rs/t/formalmethods