These requirements of much testing of inherently multithreaded code with a lot riding on not destroying user data suggests a model checker would be an essential piece, perhaps someone more knowledgeable can opine.