The Protocol Implementation Risk: Formal Verification section should contain a link to helpful background material on formal verification. The section could be enhanced to provide a more comprehensive analysis of the advantages and pitfalls of formal analysis. Links to common tools that could be used for formal analysis should also be included.