Given the data-race-freedom guarantees of Rust's non-unsafe code, one might reasonably argue that there is no point in the Kernel Concurrency Sanitizer (KCSAN) analyzing such code. However, the Linux kernel is going to need unsafe Rust code, and although there has been significant progress in formal verification of such code, one of the leading...