5 ms·

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 litt

• mirashii 5mo ago
  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 5mo ago
    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.
  • deleted 5mo ago
    [deleted]
• yencabulator 5mo ago
  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.