The specification can be model checked, but we don't have a machine-checkable proof. I agree that that would be very useful, and we'll think about writing one at some point in the future.
Whoops, Iulian's correct - I was being imprecise earlier. We have a formal specification in TLA+ that we put through the TLC model checker for several weeks of runtime on the biggest machine we could find, not a machine-checkable proof.
But to the original questioner, yes, we should put the TLA+ spec online instead of requiring someone to copy/paste from the tech report... please hold. :)
But to the original questioner, yes, we should put the TLA+ spec online instead of requiring someone to copy/paste from the tech report... please hold. :)