Some new developments of the framework in the last two years:

- packaging via OPAM to separate framework code and system code

- support for specifying and proving liveness properties

- support for proving Abadi/Lamport style refinement mappings between systems

The following workshop paper gives an overview of current and upcoming work: http://conf.researchr.org/event/CoqPL-2017/main-verification...