Coq is the one I use most. I've heard of lean as well though. Those are both proof assistants not theorem provers. Dafny uses z3 to attempt to automatically pr

Coq is the one I use most. I've heard of lean as well though. Those are both proof assistants not theorem provers. Dafny uses z3 to attempt to automatically prove theorems about your code. Lean or Coq (for the most part) require that you write the proofs manually in a special language they provide and they will tell you whether or not your proof has errors. In general these languages lie on a spectrum between more automatic to more manual with the automatic ones taking potentially more time and being more limited but requiring less of you and the manual ones such as lean or coq are more expressive but harder to use because you have to provide all of the proofs. I should say all this with the caveat that I'm only learning these things now so I've probably said something wrong. Please correct me if that is the case.