Using Rust in Linux aims to create more solid, secure code: avoiding memory safety issues and concurrency issues by taking advantage of Rust's language features and by designing a safe API for drivers to use. This talk examines how / whether we can go further using automatic formal verification tools.
Can we go beyond the checks that Rust provides? What additional checks would we want to perform? What can be done using the tools that exist today? What needs to be done to make this useful to developers? (Spoiler: we are not there yet)