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.

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.