[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

[mirashii]

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.

[scott_w]

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.

[yencabulator]

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.