No. I've only seen two, formal verifications of secure email with neither being PGP. I can't find the link to one but the other of Privacy-Enhanced Mail is here

No. I've only seen two, formal verifications of secure email with neither being PGP. I can't find the link to one but the other of Privacy-Enhanced Mail is here: https://pdfs.semanticscholar.org/b6e2/3ac057b8716ebd4ab7831f4c4e03bdad59d4.pdf https://pdfs.semanticscholar.org/b6e2/3ac057b8716ebd4ab7831f... They use Kesterel's Specware tools to essentially turn it from HOL properties to a formal design with code generation following. Kesterel was kind enough to open-source some of their stuff: https://github.com/KestrelInstitute/Specware/ https://github.com/KestrelInstitute/Specware/ However, recent results in other tooling suggest the best way to go about it would be using tools like F* in miTLS, CRYPTOL, SPARK Ada, and/or Frama-C. Each component of a basic, subset of PGP has already been verified in isolation. Now, the algorithms just need to be fed into such tools, the protocol speced out miTLS-style, the integration proven sound, and object code shown to match the source. It looks doable with today's formal methods. More a matter of available labor and interest.