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 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.