[ivanbakel]

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?

[adreid]

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.