If you've got a provably secure protocol, what's the problem with formally verifying the implementation of the protocol?
I work in an area where bugs are very scary, so we use formal verification, and that's on top of having many more testers than developers.
From the perspective of this naive outsider, I'd would have expected FV to be worth it for security sensitive protocols. Is it that the protocols are too complex to be verified, or is it just not considered to be worth the effort?