This is more at the end of automatic verification tools like KLEE, SMACK, etc.
Auto active tools like Prusti are super-interesting too and I suspect that we need a hybrid approach.
From what I understand of Prusti, it still aims to be automatic and the underlying Viper pipeline still relies on constraint solving for the most part - certainly the Prusti examples don't seem to do anything more complex than that.
Would you be able to outline the main differences?
The difference is really about the level of annotation you provide. In testing (and the more automated verifiers) you might add assertions. In the “auto active” tools, you are adding more function contracts, invariants, maybe hints to help find a proof, etc.
Would you be able to outline the main differences?