Is there any work being done to formally prove GnuPG' algorithms correctness? Just curious since there are other topic around Coq in the front page and I couldn't find much by searching.
They should use cryptol instead which was recently open sourced.
Algorithmic correctness is probably less interesting than the presence of side-channels nowadays, and that's far, far, far harder to model.
I do know of one researcher working on this: Julian Bangert at MIT out of Dartmouth has modeled x86 family processors in SMT, and is able to prove that all paths through a particular piece of code compile so that all cache hits are identical, CPU ticks are identical, etc. Brilliant young man - I expect we'll be seeing a lot more from him.