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.

Edit:

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;
            }
        }
    }

~~Kani is very unlikely to find x=1023.~~

https://model-checking.github.io/kani/tutorial-first-steps.h...

Kani will find 1023 unless you constrain the input. The link you posted is saying a property test is unlikely to find it but Kani will find it.

Yeah you misread that. Read it again, it's saying normal fuzzing is unlikely to find it but Kani finds it instantly.

Oh this is embarrassing.