Comment by YorkshireSeason

One should also mention Isabelle/HOL [1] and Concrete Semantics [2]. As of May 2018, Isabelle/HOL has the best proof automation, in case you want to get things done.

[1] https://isabelle.in.tum.de/