Isn't this line incorrect?

    BB == b > 1 /\ b' = b - 2 /\ w' = w + 1           \* Picked 2 black

The state would be valid. If b > 1 then there are at least two (b > 1 is equivalent to b >= 2 here since b must be a non-negative integer). Remove two (b' = b - 2) and add one white (w' = w + 1). If b == 2, then we still end in a valid state, it'll just be (b = 0 & w' = w + 1).

EDIT: Actually, the original spec doesn't even say what is a valid state after initialization. It provides only a requirement on the initial state (that w + b > 0 and that w and b are both in Nat, or >= 0, when initialized). The correctly formulated rules ensure that w and b remain in Nat, but there's no other piece of the specification that seems to require it.

Once the author starts adding invariants (like NotEmpty) that adds a requirement that w + b > 0 remains true for ever, but since w is incremented and b is decremented, even BB results in NotEmpty remaining satisfied. Each of the steps does, since they all add one bean back.