Note This article describes my attempt, in the summer of 2015, to develop a modular version of Verdi, a framework for verified distributed systems in Coq. The dream of a modular Verdi has now been achieved, in a more complete and interesting way than in this work, by my friends Ilya Sergey, James R. Wilcox, and Zachary Tatlock in their DiSeL system (first described at SNAPL’17 and then published in full detail at POPL’18). This article demonstrates one alternate idea, and highlights the d...
