I do. I think that security-critical but overly complex software like this should be rewritten and certain aspects of it formally verified, since such things are now practical.