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!