[at_compile_time]

I hadn't heard of ATS before, and I think that I mistook your using it as an example of "more isn't always better" and thought you were suggesting it as an actual alternative.

I'm looking for the next thing I want to learn, and have been leaning towards logic programming and theorem provers, so you inadvertently piqued my interest.

[pron]

Sure, just keep in mind that various formal verification tools vary greatly in their usability, even theorem provers. I.e. the experience with ATS will be quite different from Lean, which will be quite different from TLA+.