Verus is a tool for verifying the correctness of code written in Rust
by fanf2 on 4/20/2026, 8:42:05 PM
https://verus-lang.github.io/verus/guide/
Comments
by: 6r17
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
4/23/2026, 3:48:14 AM
by: suobset
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.
4/23/2026, 2:59:30 AM
by: isubasinghe
Oh hey I worked on this :)
4/23/2026, 2:23:13 AM
by:
4/23/2026, 4:04:16 AM
by: esafak
<a href="https://github.com/verus-lang/verus" rel="nofollow">https://github.com/verus-lang/verus</a>
4/23/2026, 3:03:40 AM
by: himata4113
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.<p>I do see a value in validating constraints, but the examples are either too simple or I'm too dumb.
4/23/2026, 3:16:20 AM