And with SPARK if you want to dive into manual proof of a property (usually because SPARK & Why3 and all the SMT solvers can't manage and you don't have some appropriate lemmas) with Coq or Isabelle.

Some introduction https://blog.adacore.com/using-coq-to-verify-spark-2014-code (from 2014, so probably much improved since).

And some examples : http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_...

Not the best way to learn manual proof, but I've seen it used very efficiently.

But then if course you're faced with the difficulty of increasing automation : the more you automate, the more it is difficult to have the 'muscle memory' (and lower cognitive load) that you get when flexing the manual proof often...