I tried this code:

#[cfg_attr(kani, kani::proof)]
fn main() {
    let s = "foo";
    assert!(1 + 1 == 3, "arg is {}", s);
}

using the following command line invocation:

kani assert_arg.rs

with Kani version: 8b1d18c

I expected to see this happen: No warnings

Instead, this happened: Kani emits the following spurious warning:

warning: unused variable: `s`
 --> assert_arg.rs:3:9
  |
3 |     let s = "foo";
  |         ^ help: if this is intentional, prefix it with an underscore: `_s`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: 1 warning emitted

This is due to Kani's overridden assert macros which stringify the arguments during macro expansion, but do not use the actual arguments in the expansion.