Making Even Safe Rust a Little Safer: Model Checking Safe and Unsafe Code Whenever invariants can be expressed as proofs rather than as tests that may or may not be exhaustive, the mathematical guarantees of model checkers will provide stronger assurances the code is correct.
Making Unsafe Rust a Little Safer: Tools for Verifying Unsafe Code, Including Libraries in C and C++ This article will look at tools for verifying unsafe Rust code, including unsafe code called from libraries written in C or C++.
Future Software Should Be Memory Safe: Reflections on A Path Toward Secure and Measurable Software Future software should be memory safe, but secure code is about a lot more than memory safety.
