I tried this code:

#[kani::proof]
fn check_out_of_bounds() {
    let mut bytes = kani::slice::any_slice::<u8, 5>();
    let val = unsafe { *bytes.get_slice().as_ptr().add(4) };
    kani::assume(val != 0);
    assert_ne!(val, 0);
}

using the following command line invocation:

kani check.rs

I expected to see this happen: I expected that accessing position 4 of any_slice may fail with out of bounds access.

Instead, this happened: The verification succeeded. Because any_slice always allocates a buffer with size MAX_SIZE (in this case 5), the access to position 4 is always valid.