Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.