Verus is a tool for verifying the correctness of code written in Rust

(verus-lang.github.io)

34 points | by fanf2 2 days ago

6 comments

  • 6r17 57 minutes ago
    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
  • suobset 1 hour ago
    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.
  • isubasinghe 2 hours ago
    Oh hey I worked on this :)
  • esafak 1 hour ago
  • himata4113 1 hour ago
    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.