Making Even Safe Rust a Little Safer: Model Checking Safe and Unsafe Code

In my last article, I explored tools that can help ensure unsafe code in Rust is free from security vulnerabilities caused by undefined behaviours. These tools included sanitizers for memory and concurrency errors, and Miri, an interpreter focused on detecting undefined behaviours.