Kani Verifier Blog

But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests. Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/ In Kani, a proof looks like this https://github.com/model-checking/verify-rust-std/blob/00169b76e90ab44… #[kani::proof_for_contract(NonNull::new_unchecked)] pub fn non_null_check_new_unchecked() { let raw_ptr = kani::any::<usize>() as *mut i32; unsafe { let _ = NonNull::new_unchecked(raw_ptr); } } It looks like a test, but actually it is testing that every possible usize, when converted to a pointer to i32 and built with NonNull::new_unchecked, will follow the contract of NonNull::new_unchecked, which is defined here https://github.com/model-checking/verify-rust-std/blob/00169b76e90ab44… #[requires(!ptr.is_null())] #[ensures(|result| result.as_ptr() == ptr)] Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptr That's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the…

Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of [0] https://github.com/model-checking/kani [1] https://model-checking.github.io/cbmc-training/cbmc/overview/goto-prog…

The tutorial is helpful: https://model-checking.github.io/kani/kani-tutorial.html Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/

Yeah and at the same time there are efforts to verify standard library using Kani: https://model-checking.github.io/verify-rust-std/ Between this and Bjarne Stroustrup panic leaked email to C++ standards committee members, it's going to be interesting for Rust's future.

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.html

Uninitialized local variables are documented as a source of a certain type of nondeterminism: http://www.cprover.org/cprover-manual/modeling/nondeterminism/ So the checker treats them as defined, but with an unknown variable. You could have written this instead: extern int unknown_int_value(void); int x = unknown_int_value(); And leaving unknown_int_value undefined (so it's not visible to the analyzer). Or write a function and use x as a parameter. I suspect CBMC does this to have a convenient syntax for this frequent scenario. Apparently, it's used quite often, as in these examples: https://model-checking.github.io/cbmc-training/cbmc/overview/proof.htm… It seems that CBMC is not intended to check production sources directly against C semantics, but to prove things about programs written in a C-like syntax.

Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html Some crypto, AWS common C, FreeRTOS. Other interesting applications https://www.cprover.org/cbmc/applications/

Looks like that the project has changed its name from "rmc" (Rust Model Checker) to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani) and https://model-checking.github.io/rmc/ (404). Anyone knows why?

The primary thing it checks for is panics. (bounds|overflow|DBZ) are just examples where Rust panics (for overflows rust doesn't always panic, while Kani always fails). You aren't testing your application code directly, but writing a test function. That test function can include any assertion you want in the end, which causes a panic, failing the verification. Similarly you want to add assumptions in the test function for pre-conditions, so parameter verification assertions in the application won't fail the verification. Example from the tutorial: #[cfg(kani)] #[kani::proof] fn verify_success() { let x: u32 = kani::any(); // estimate_size rejects x >= 4096, so this prevents failure from argument verification panicking kani::assume(x < 4096); let y = estimate_size(x); assert!(y < 10); } https://model-checking.github.io/kani/tutorial-first-steps.html

There are so many Rust things that Prusti doesn't understand that applying it to any real world project is still extremely challenging. Kani interacts a little better with real code (see https://model-checking.github.io/kani/rust-feature-support.html), as long as you don't accidentally need e.g. randomness for HashMap DoS protection (https://github.com/model-checking/kani/issues/2423#issuecomment-192550… Loops are an utter pain to prove with Kani, though: https://model-checking.github.io/kani/tutorial-loop-unwinding.html -- I believe people are using Verifast for loop-heavy code instead: https://github.com/verifast/verifast (this hole patchwork of multiple tools mostly consumed as binary downloads is miserable) Here's an attempt to gradually verify the Rust stdlib: https://github.com/model-checking/verify-rust-std

My own list, which is pretty different in character than Derek's. Gankra's work on a useful rust memory model is both fascinating and useful: https://twitter.com/Gankra_/status/1509335163045650436 This tool to convert low-complexity rust tests to proofs is interesting and something I'm glad I know exists: https://model-checking.github.io/kani-verifier-blog/2022/05/04/announc… I'm using this code I found out about via reddit in a side project, probably less interesting to you though: https://github.com/setzer22/egui_node_graph (Warning, videos from here on out): Cool product demo of a futuristic debugger: https://www.hytradboi.com/2022/debugging-by-querying-a-database-of-all… These people also have a cool demo of splitting a single program across two different computers (frontend and backend webserver in their case). Maybe a bit less convincing than the previous one, but something I intend to watch: https://www.hytradboi.com/2022/uis-are-streaming-dags These people have some really cool work on automatically solving physics problems (just linking to one of their talks as an example): https://www.youtube.com/watch?v=WHhDgxkiR9c