Hacker News Reader

Comment by 6r17 | Hacker News Reader

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

View on HN

Do you have any reference to the Rust community “not allowing” something? This seems more like a case of a relatively niche tool doing what it needed to do to work, but not (yet) some broader effort to upstream or integrate this into cargo or rustup. I couldn’t find any RFCs or anything, for instance.

I didn’t read OP as saying “the community won’t allow” but more “the tooling doesn’t allow” for what they want to do.

So far out of what I've looked at, Kani blends into the Rust language best. Verified code snippets look a lot like unit tests.

  #[kani::proof]
  fn check_my_property() {
     // Create a nondeterministic input
     let input: u8 = kani::any();

     // Call the function under verification
     let output = function_under_test(input);

     // Check that it meets the specification
     assert!(meets_specification(input, output));
  }

It looks like fuzzing, but it's proving no-panic for all possible values symbolically. If only it handled loops better :-/

Verus wraps everything in its macro that makes rust-analyzer etc unhappy.

Reply on news.ycombinator.com