All I mean is that the evidence is no matter how much you care about getting it right, it will take several years to get this kind of system right. That was goo

All I mean is that the evidence is no matter how much you care about getting it right, it will take several years to get this kind of system right. That was google and everyone else's experience with just Paxos, let alone a larger system that also involves time synchronization, transaction protocols, etc. I don't think it was a matter of "ooops, we just didn't care enough". There's no way to make this kind of thing where it comes out of the oven perfect the first time. There just isn't. I agree that using TLA+ or the like from the very beginning would probably help. I also found the "rule based development" paper from the RAMCloud folks pretty convincing, but I haven't tried to put it into practice.