Abstraction, Refinement and Proof for Probabilistic Systems presents a rigorous approach to modeling and reasoning about computer systems that incorporate probability. Its foundations lie in traditional Boolean sequential-program logic - but its extension to numeric rather than merely true-or-false judgments takes it much further, into areas such as randomized algorithms, fault tolerance and, in distributed systems, almost-certain symmetry breaking.