I don't really have an opinion either way, having never tried TDD, but I do write distributed systems and don't see why you can't use post-facto testing to get the same results. I am interested in your reasoning. (Re: Proof, http://pdos.csail.mit.edu/6.824/schedule.html doesn't feature the word 'test' which though circumstantial sort of downplays the weight of an inextricable link such as that you are supposing.)
It sounds like the non-test specification is simply poor, and the tests elucidate parts of the specification that are unclear. This doesn't seem relevant to the original question of the claimed requisite-level efficacy of TDD in designing distributed systems.
Actually, the specifications are quite clear. The subject matter is just difficult to implement correctly. I encourage you to try it. It's a lot of fun.
