In this paper, we present a push-button, automated technique for verifying $\epsilon$-differential privacy of sophisticated randomized algorithms. We make a range of conceptual, algorithmic,and practical contributions: (1) Inspired by the recent advances on approximate couplings and randomness alignment, we present a new proof technique called coupling strategies, which casts differential privacy proofs as discovering a strategy in a game where we have finite privacy resources to expend. (2) To discover a winning strategy, we present a constraint-based formulation of the problem as solving a set of Horn modulo couplings (HMC) constraints, a novel kind of constraints combining first-order Horn clauses with probabilistic constraints. (3) We present a technique for solving HMC constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (4) Finally, we implement our technique and provide the first automated proofs of a number of algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism.