GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. As an example of how far we can go to guide the proof, see the paper we are presenting at NASA Formal Methods symposium 2017. It describes how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification. The code presented in this paper is available as a distributed example in the SPARK github repository and is described in the SPARK user guide (see 'red_black_trees').