[nano_o]

Great work. Do you have a link to the machine-checked proof? In the technical report there is only a formal specification and a detailed but not machine-checkable proof. It would be really great to see systems researchers write machine-checked proofs :)

[imoraru]

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.

[dgacmu]

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. :)

[dgacmu]

The TLA+ spec is now in the git repository. Thanks for the suggestion!