Verification results

Running Kani on a harness produces an output that includes a set of checks as follows:

RESULTS:
Check 1: example.assertion.1
         - Status: <status>
         - Description: <description>
         - Location: <location>
[...]

Kani determines the verification result for the harness based on the result (i.e., <status>) of each individual check (also known as "properties"). If all checks are successful then the overall verification result of the harness is successful. Otherwise the verification fails, which indicates issues with the code under verification.

Check results

The result (or Status) of a check in Kani can be one of the following:

SUCCESS: This indicates that the check passed (i.e., the property holds). Note that in some cases, the property may hold vacuously. This can occur because the property is unreachable, or because the harness is over-constrained.

Example:

fn success_example() {
    let mut sum = 0;
    for i in 1..4 {
        sum += i;
    }
    assert_eq!(sum, 6);
}

The output from Kani indicates that the assertion holds:

Check 4: success_example.assertion.4
         - Status: SUCCESS
         - Description: "assertion failed: sum == 6"

FAILURE: This indicates that the check failed (i.e., the property doesn't hold). In this case, please see the debugging verification failures section for more help.

Example:

fn failure_example() {
    let arr = [1, 2, 3];
    assert_ne!(arr.len(), 3);
}

The assertion doesn't hold as Kani's output indicates:

Check 2: failure_example.assertion.2
         - Status: FAILURE
         - Description: "assertion failed: arr.len() != 3"

UNREACHABLE: This indicates that the check is unreachable (i.e., the property holds vacuously). This occurs when there is no possible execution trace that can reach the check's line of code. This may be because the function that contains the check is unused, or because the harness does not trigger the condition under which the check is invoked. Kani currently checks reachability for the following assertion types:
1. Assert macros (e.g. assert, assert_eq, etc.)
2. Arithmetic overflow checks
3. Negation overflow checks
4. Index out-of-bounds checks
5. Divide/remainder-by-zero checks

Example:

fn unreachable_example() {
    let x = 5;
    let y = x + 2;
    if x > y {
        assert!(x < 8);
    }
}

The output from Kani indicates that the assertion is unreachable:

Check 2: unreachable_example.assertion.2
         - Status: UNREACHABLE
         - Description: "assertion failed: x < 8"

UNDETERMINED: This indicates that Kani was not able to conclude whether the property holds or not. This can occur when the Rust program contains a construct that is not currently supported by Kani. See Rust feature support for Kani's current support of the Rust language features.

Example:

fn undetermined_example() {
    let mut x = 0;
    unsupp(&mut x);
    assert!(x == 0);
}

#[feature(asm)]
fn unsupp(x: &mut u8) {
    unsafe {
        std::arch::asm!("nop");
    }
}

The output from Kani indicates that the assertion is undetermined due to the missing support for inline assembly in Kani:

Check 2: undetermined_example.assertion.2
         - Status: UNDETERMINED
         - Description: "assertion failed: x == 0"

Cover property results

Kani provides a kani::cover macro that can be used for checking whether a condition may occur at a certain point in the code.

The result of a cover property can be one of the following:

SATISFIED: This indicates that Kani found an execution that triggers the specified condition.

The following example uses kani::cover to check if it's possible for x and y to hold the values 24 and 72, respectively, after 3 iterations of the while loop, which turns out to be the case.

#[kani::unwind(256)]
fn cover_satisfied_example() {
    let mut x: u8 = kani::any();
    let mut y: u8 = kani::any();
    y /= 2;
    let mut i = 0;
    while x != 0 && y != 0 {
        kani::cover!(i > 2 && x == 24 && y == 72);
        if x >= y { x -= y; }
        else { y -= x; }
        i += 1;
    }
}

Results:

Check 1: cover_satisfied_example.cover.1
         - Status: SATISFIED
         - Description: "cover condition: i > 2 && x == 24 && y == 72"
         - Location: src/main.rs:60:9 in function cover_satisfied_example

UNSATISFIABLE: This indicates that Kani proved that the specified condition is impossible.

The following example uses kani::cover to check if it's possible to have a UTF-8 encoded string consisting of 5 bytes that correspond to a string with a single character.

#[kani::unwind(6)]
fn cover_unsatisfiable_example() {
    let bytes: [u8; 5] = kani::any();
    let s = std::str::from_utf8(&bytes);
    if let Ok(s) = s {
        kani::cover!(s.chars().count() <= 1);
    }
}

which is not possible as such string will contain at least two characters.

Check 46: cover_unsatisfiable_example.cover.1
         - Status: UNSATISFIABLE
         - Description: "cover condition: s.chars().count() <= 1"
         - Location: src/main.rs:75:9 in function cover_unsatisfiable_example

UNREACHABLE: This indicates that the cover property itself is unreachable (i.e. it is vacuously unsatisfiable).

In contrast to an UNREACHABLE result for assertions, an unreachable (or an unsatisfiable) cover property may indicate an incomplete proof.

Example: In this example, a kani::cover call is unreachable because if the outer if condition holds, then the non-empty range r2 is strictly larger than the non-empty range r1, in which case, the condition in the inner if condition is impossible.

#[kani::unwind(6)]
fn cover_unreachable_example() {
    let r1: std::ops::Range<i32> = kani::any()..kani::any();
    let r2: std::ops::Range<i32> = kani::any()..kani::any();
    kani::assume(!r1.is_empty());
    kani::assume(!r2.is_empty());
    if r2.start > r1.end {
        if r2.end < r1.end {
            kani::cover!(r2.contains(&0));
        }
    }
}

Check 3: cover_unreachable_example.cover.1
         - Status: UNREACHABLE
         - Description: "cover condition: r2.contains(&0)"
         - Location: src/main.rs:90:13 in function cover_unreachable_example

UNDETERMINED: This is the same as the UNDETERMINED result for normal checks (see [check_results]).

Verification summary

Kani reports a summary at the end of the verification report, which includes the overall results of all checks, the overall results of cover properties (if the package includes cover properties), and the overall verification result, e.g.:

SUMMARY:
 ** 0 of 786 failed (41 unreachable)

 ** 0 of 1 cover properties satisfied


VERIFICATION:- SUCCESSFUL

The Kani Rust Verifier

Verification results

Check results

Cover property results

Verification summary