Formal verification would not help if the formal or informal design specs called for unauthenticated telnet. It would prove that the entire stack was bullet-proof against memory violations and mathematically pure, and that it would with 100% certainty allow untrusted users to access administrative functions.