> Is this behaviour documented? Or are you just expected to know what C does?

Indeed, it's not as well documented as it should be. I think that's partly for historical reasons: before Python 2.7, Python's % formatting more-or-less delegated directly to the underlying C sprintf library function, and so just inherited whatever the behaviour of that function happened to be on the target operating system. Because the C standard doesn't make guarantees about the behaviour of %f for ties, Python wasn't in a position to do so either.

But that excuse doesn't work any more with Python 2.7 and Python 3.x, where on most (but still not all) platforms, we're consistently rounding results using the usual round-ties-to-even rounding mode.

There's a currently open issue (#17259) to improve the documentation here.