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 pro

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-of-implementations-of-distributed-systems-under-churn http://conf.researchr.org/event/CoqPL-2017/main-verification...