Over the past decade, open source model checking tools have matured to the point that they can be used as a practical means of formally verifying software. Model checking can verify memory safety, UB safety, function / interface contracts, and invariants in existing software written in C, C++, and Rust.
This talk demonstrates model checking in a FreeBSD userland utility, a simple BCHS application, and a kernel module. Source code will be provided.