I'm not sure what you're implying. Kani absolutely is formal verification. CBMC stands for C Bounded Model Checker and model checking is one of the main forms of formal verification.
Seems like I misread the documentation...
~~What I was implying is that Kani just can't figure out all of the paths;~~ ~~Consider this example from Kani documentation [1]:~~
fn estimate_size(x: u32) -> u32 {
if x < 256 {
if x < 128 {
return 1;
} else {
return 3;
}
} else if x < 1024 {
if x > 1022 {
panic!("Oh no, a failing corner case!");
} else {
return 5;
}
} else {
if x < 2048 {
return 7;
} else {
return 9;
}
}
}
https://model-checking.github.io/kani/tutorial-first-steps.h...