A Coq framework for correct-by-construction derivation of distributed system protocols

We are designing a formal synthesis framework, embedded in Coq, for building proven-to-be-correct message-passing systems. The framework provides a way of specifying protocols at a high-level. A synthesizer tries to build an executable implementation that is formally proven to follow the specification. Synthesized implementations may involve a lot of interleavings, where the safety of such interleavings is automatically guaranteed by the synthesis process. As a case study, we are currently trying to synthesize various cache-coherence protocols.