The B Method does not currently handle probability. We add it in a limited form, concentrating on "almost-certain" properties which hold with probability one; and we address briefly the implied modification to the programs that support B.
The Generalised Substitution Language is extended with a binary operator (+) representing "abstract probabilistic choice", so that the substitution prog_1 (+) prog_2 means roughly "choose between prog_1 and prog_2 with some probability neither one nor zero". We then adjust B's proof rule for loops --- specifically, the variant rule --- so that in many case, it is possible to prove "probability-one" correctness of programs containing the new operator, which was not possible in B before, while remaining almost entirely within the original Boolean logic.
Applications include probabilistic algorithms such as the IEEE 1394 Root Contention Protocol ("Fire Wire") in which a probabilistic "symmetry-breaking" strategy forms a key component of the design.