That looks amazing. You should shoot an email to Yannick Moy! He had lots of insights and ideas on how to help automatically generate or infer (reliably) loop variants/invariants (they use loop unrolling for example: https://blog.adacore.com/proving-loops-without-loop-invarian...) .

I know AdaCore uses CodePeer (abstract interpretation and iirc 'interval propagation') to help SPARK avoid or simplify some VCs and it helps in a lot of cases.

There's also some possibilities with symbolic execution, maybe on the counter-examples generation side.

I think you're treading a very interesting path!