It seems to me that all of these approaches are very limited in scope (mainly linear arithmetic), and only capable of analysing pretty simple programs. That's n

It seems to me that all of these approaches are very limited in scope (mainly linear arithmetic), and only capable of analysing pretty simple programs. That's not the kind of induction proofs I deal with on a daily basis, which prove arbitrary mathematical theorems. For those things you need to use just hard manual sweat work.