[ivanbakel]

I'm pleased to see that "verification" isn't just relying on random value generators for property testing in this case. While I agree with the author that actually running code is still useful, simple specifications have the power to be much more than glorified fuzzing - and Rust is the perfect language to start pushing that in. The use of native syntax for int value ranges is especially nice.

The main question is: how does this compare to other Rust verification efforts[0]? Having to write specifications in test crates rather than next to the function definitions is probably going to be a big obstacle to multi-crate verification.

[0]: https://github.com/viperproject/prusti-dev/

[adreid]

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.

[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.

[baby]

Check mirai https://github.com/facebookexperimental/MIRAI