I previously worked on proving information flow analyses in Coq in cooperation with
the group from Princeton as well as
John Hatcliff,
Torben Amtoft, and
Zhi Zhang from Kansas State.
Papers and slides :
Mostly Sound Type System Improves a Foundational Program Verifier In CPP 2013
(paper)