Agreed with Tim Peters about this not being possible with fully compliant IEEE 754 arithmetic (see http://stackoverflow.com/a/3041071/270986 for a sketch of a proof), but it's certainly a possibility with double rounding, as Steven's result demonstrates.  And 32-bit Linux is currently the worst offender for double rounding: IIRC OS X uses the SSE2 instructions exclusively for floating-point arithmetic, and 64-bit Linux tends to do the same.  Windows uses the x87 FPU, but sets the FPU precision to 53-bits, so you don't see double rounding within the normal range (though it's still possible with computations having subnormal results).

So I'd say that yes, this *is* a bug in random.choice, though it's one that should show up very rarely indeed.