Systems that need to be robust to crashes often implement complex recovery procedures so that they are always able to return to well behaved states without losing all progress made before the crash. Work on verification of these systems has relied on complex operational semantic models with intricate and brittle proofs of correctness, and often has not been mechanized due to the complexity of the proofs and relying on hard to formalize assumptions. Simulation relations offer a promising way of reasoning about the complex control flows that are introduced by failures and recovery procedures by allowing the proofs to be structured as an interactive exploration of what states such failures leave the system in. However, prior work on mechanized verification using coinductive simulations does not account for reasoning about nondeterminism in a way that properly captures the semantics of nondeterministic failures. I will discuss the progress that has been made towards creating simulations that are able to properly account for nondeterministic failures.