Documentation produced that way is actually consistent with the statement you first quoted. I think what is happening here is that the researchers, being properly careful, verified what the software does, rather than trust to descriptions by others.

If there had been a formal specification, I imagine they would have both analyzed the specification for vulnerabilities, and checked the code for correct implementation.