I tried it not long ago - it's really cool just a tad sad that the rust eco-system didn't allow verus to be more streamlined in the tool and requires these little shenanigans with a different build of it - it felt a bit clunky to swap cargo for the verus one ; but the tool is definitely needed right now

I just attended a talk at Northeastern (Boston) on Verus, it's genuinely amazing. I have been using it on my own Rust codebases for a while, and it has made me think deeper about the structure and semantics of Rust code.

Oh hey I worked on this :)

Clippy with unstable features enabled catches most if not all of these cases automatically? This seems like it needs more work to do the same thing clippy does.

I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.