<p>Fault-tolerant behavior is prevalent in many fields of critical software systems. The complexity of such systems necessitates rigorous techniques for ensuring correct and reliable operation. Performing design reviews by experts is the conventional method in the industry, but it is hard to substantiate the completeness of the result. We performed a multi-year study with an automotive supplier on supporting standard-mandated safety evaluations with model checking in the context of a critical steer-by-wire function. However, existing formal verification methods returned too many redundant violations that the engineers deemed unrealistic or acceptable. Based on these findings, we propose a new process focusing on systematic, iterative exploration of distinct requirement violation scenarios with model checkers to aid the design and verification of fault-tolerant safety-critical software systems. The main challenge lies in the need to find all essentially distinct problems of subsystems without enumerating the potentially infinitely many problematic execution paths. The novelty of our approach is using abstract scenario descriptions constraining the model checker to unknown violations while allowing some violations to be categorized as acceptable by subject experts. Our approach has multifold benefits: It turns implicit assumptions into formalized environmental models and scenario descriptions, sheds light on hard-to-find requirement violations, and can be integrated into existing development processes. We present the applicability of our approach in the automotive study, where it revealed previously unknown problems in the system design and gave formal proofs to help the engineers negotiate with the client regarding required modifications.</p>