Proof automation can substantially increase productivity in the formal verification of complex systems. However, the unpredictability of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. Here, we propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce decidable verification conditions. Decidability greatly improves the predictability of proof automation, resulting in a more practical verification approach. We apply this methodology to develop verified implementations of distributed protocols with competitive performance, showing its effectiveness