To me, one of the most intimidating parts of getting into formal verification is deciding which system to use - as you mentioned, there are several. What are the strengths and weaknesses of each?
Hahahaha good catch. Perhaps if I'd used Lean on that string it wouldn't have happened.
I think the big choice is between using lightweight or heavy tools. Things like Coq and Agda take a lot of time to learn and implement but can derive 'correctly Haskell code which you can use, while TLA+ is more like a blueprint tool to check an algorithm before you write it in {favourite_language}. I think it's practical to learn TLA+ but if it's purely for intellectual satisfaction Wadler has a good book called Programming Foundations in Agda (I think?) which is available for free online.
I've heard that ACL2 is also a thing that exists.
To me, one of the most intimidating parts of getting into formal verification is deciding which system to use - as you mentioned, there are several. What are the strengths and weaknesses of each?