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.
Check mirai https://github.com/facebookexperimental/MIRAI