Thanks for the feedback.
As for #3, unfortunately we don't currently have plans to publish a formal proof (we're building a product). Some of our internal documentation is more formal, but we decided on a more readable presentation for this paper.
As for #3, unfortunately we don't currently have plans to publish a formal proof (we're building a product). Some of our internal documentation is more formal, but we decided on a more readable presentation for this paper.
Unless you already have it but don't plan to publish, which seems a little odd to me. I get that you want readable documentation, but at least you could link to it somewhere for people who go digging.
On the other hand a logical model can be encoded in a rather short amount of time by someone who is doing it periodically.
This hypothetical guy could benefit from this activity by co-authoring the paper. Original authors would benefit from it by reinforcing both the protocol and the paper.