Is there a reason a crypto messenger team wouldn't seem to publish their protocol specs using BAN notation that people can objectively reason about, and then ve

Is there a reason a crypto messenger team wouldn't seem to publish their protocol specs using BAN notation that people can objectively reason about, and then verify the implementation of it in the code? As in, if you can't explain it this clearly, what's the problem? http://www.lsv.fr/Software/spore/table.html http://www.lsv.fr/Software/spore/table.html Having worked on some crypto projects, the admonition to, "just read the code," is disingenuous, because without a formal spec, you have nothing to compare the code to or evaluate the code against.