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

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