You will probably find it valuable to write that proof. Sometimes an edge case pops up or you end up proving that it doesn't work as expected. I've done this a few times in my work.

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.

Well personally I would rather suggest to write a model, not a rigorous proof. A formal proof of any real protocol is both long and tedious journey; production guys will hardly find it useful thing to do.

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.