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++.
Is the Scientific Method Valuable in Engineering? In engineering, fixating on a hypothesis, and working to confirm or falsify it, can lead us astray.