This is achieved by latching on to rustc, and then compiling to gotoc, which is then used with CBMC.

Removed due to my misunderstanding:

~~I don't think Kani counts as a "formal" verification tool, emphasis on "formal", but it is a verification tool for rust code and is powered by CBMC.~~

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.

Some other tool (Coq-based) to formally verify unsafe Rust https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev