We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using the new notion of failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: (i) we exploit program synthesis methods to select and instantiate axioms about sampling instructions, and then (ii) utilize Craig interpolation to show that traces failing the target specification occur with small probability. Our logical method naturally handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to be able to automatically establish accuracy properties of such sophisticated algorithms.