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 ap

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 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_example/manual_proof.html 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...