Iddqd, or the hardest kind of unsafe Rust

The section on how to do software assurance of unsafe code in Rust is excellent.

A lot of prior guidance I've seen tends to stop at the level of running Miri, but (as the article says) there are things Miri won't catch. The model-based tests with a known-good oracle and the use of fault injection (especially panic-related behavior) are really good.

Safety in the face of panics in Rust can be hard to reason about, and the standard library itself has made errors with those semantics in the past.

Great work Rain and Oxide for building something so useful and assuring it so robustly!