I tried this code:

#[kani::proof]
fn check_i8() {
    let v1: i8 = -10;
    let n1 = NonZeroI8::new(v1);
    assert!(n1.is_some());
}

using the following command line invocation:

kani test.rs

with Kani version:

I expected to see this happen: Harness should succeed.

Instead, this happened: Verification failed.

SUMMARY:
 ** 1 of 8 failed
Failed Checks: assertion failed: n1.is_some()
File: "/kani/tests/kani/Invariants/check_nonzero.rs", line 25, in check_i8

VERIFICATION:- FAILED

Note that we do have a test that should be checking this (tests/kani/Invariants/check_nonzero.rs), and if you run it manually, you can see that the test is failing. However, the test uses kani::expect_fail() which is also broken. So the tests actually succeeds in our CI.