Fault-tolerance techniques are widely used to improve the resiliency of hardware/software systems. An important step for the deployment of such techniques in a concrete setting is to find reasonable configurations balancing the tradeoff between resiliency and energy. The paper reports on a case study where we employ probabilistic model checking to synthesize values for tunable system parameters of a redo-based fault-tolerance mechanism. We consider discrete parameters of a finite range (as the number of redos) as well as continuous parameters to encode the error detection rates of the underlying control- and data-flow checkers. To tackle the state-explosion problem, we exploit structural properties of redo-based protocols. The parameter synthesis approach combines probabilistic model checking for Markov chains with parametric transition probabilities and reward values and computer-algebra techniques to determine parameter valuations that minimize the expected overhead given constraints on the utility, depending on a given error probability.