  We propose a probabilistic Hoare logic aHL based on the union bound, a tool
from basic probability theory. While the union bound is simple, it is an
extremely common tool for analyzing randomized algorithms. In formal
verification terms, the union bound allows flexible and compositional reasoning
over possible ways an algorithm may go wrong. It also enables a clean
separation between reasoning about probabilities and reasoning about events,
which are expressed as standard first-order formulas in our logic. Notably,
assertions in our logic are non-probabilistic, even though we can conclude
probabilistic facts from the judgments.
  Our logic can also prove accuracy properties for interactive programs, where
the program must produce intermediate outputs as soon as pieces of the input
arrive, rather than accessing the entire input at once. This setting also
enables adaptivity, where later inputs may depend on earlier intermediate
outputs. We show how to prove accuracy for several examples from the
differential privacy literature, both interactive and non-interactive.
