The abstract of the paper [Wilcox et al., Verdi: a Framework for Implementing and Formally Verifying Distributed Systems, PLDI 2015] seemed quite exciting. Alas, I can't say I recommend reading the paper. For my taste, its information density is way too low. I can't say that I recommend reading the code either, but that's only because I didn't read it. All indications point to it being a cool thing to read.
One worthwhile thing I learned from the paper is that there is a new and cool consensus algorithm: Raft. I should probably check it out.
There is one thing that bugged me from the beginning to the end of the article. The article states that,
Verdi's key conceptual contribution is the use of verified system transformers to separate concerns of correctness and fault tolerance.
What does this mean? Basically, you implement your algorithm assuming the network is perfect. Then, if you want to run it on a network that, say, stutters, you invoke one of these transformers and you get an implementation for a stuttering network. (And, of course, the proof of correctness gets transformed as well.) That's all nice. But. But I studied networks in my undergrad degree, and I distinctly recall spending endless boring hours discussing the solution to this kind of issues: add an abstraction layer. So, naturally, I was expecting to see how this code transformation approach (which, by the way, is a functor) compares to abstraction layers. Alas, there is no mention of the latter.
This tension (between the abstraction layers that I expected and the functors I was given) reminded me of another paper on my reading list: [Gu et al., Deep Specifications and Certified Abstraction Layers, POPL 2015] . Its abstract seemed to imply that they explain how one is supposed to write formal specifications that correspond to the informal idea of abstraction layers.