Today’s most important computer systems are distributed systems: those that consist of multiple components that communicate by sending messages over a network, and where individual components or network connections may fail independently. Programming such systems is hard due to messages being reordered or delayed and the ever-present possibility of failure. Many liveness guarantees are impossible in such a setting, and even safety properties (such as “received messages arrive in the order they were sent”) can be challenging to prove. Protocols meant to ensure, say, a given message delivery order or a given data consistency policy are widely used in distributed systems, but verification of the correctness of those protocols is less common — much less machine-checked proofs about executable implementations.

Language-integrated verification techniques promise to bridge the gap between protocol specifications and executable implementations, letting programmers carry out verification directly in the same executable programming language used for implementation. One such language-level verification approach centers around refinement types: data types that let programmers specify logical predicates that restrict, or refine, the set of values that can inhabit the type, and that can be checked at compile time by an off-the-shelf SMT solver. Refinement types are beginning to make their way into general-purpose, industrial-strength programming languages through tools such as Liquid Haskell, which adds support for refinement types to the Haskell language. Liquid Haskell goes beyond last decade’s refinement types: its powerful reflection capabilities let you prove theorems in an extrinsic style, by defining Haskell functions (with help from the underlying solver). Furthermore, its integration with an existing programming language lets programmers work with pre-existing code and add richer specifications as they go. But is it up to the task of verifying interesting correctness properties of practically deployable distributed systems?

In this talk, I’ll report on my research group’s recent and ongoing efforts to answer that question in the affirmative. For example, in a messaging system consisting of several peer nodes, we can use refinement types to express properties about the order in which broadcast messages are delivered at a node, and we can use Liquid Haskell to prove those properties extrinsically. Likewise, in a replicated storage system we can express and prove properties about the convergence of replicated data structures. I’ll recount the pleasures and pitfalls of our journey so far, and discuss where we hope to go next.