Abstract

Distributed Systems are inherently hard to build and reason about. Their combination of asynchrony and partial failures leads to complex edge cases that are rarely repeatable under test conditions. To address this problem, we can use formal methods to formally model and analyze our distributed systems, detecting error scenarios before they reach production. Taking the idea further, we can compile our formal model into an implementation, minimizing the chances that our formal models and systems exhibit diverging behavior. Our compiler PGo does this, and we have used it to develop a collection formally verified distributed systems. Of those, our verified Raft-based key-value store PGo-RaftKV outperforms related work that is compiled from formal models. The story isn’t over, however. Spec-compiled code is still not performance-competitive with hand-written production systems like etcd, and spec-compiled code can still have bugs (in how the verified protocol interacts with the world). We describe our work so far, as well as follow-up work we have begun that addresses remaining shortfalls in compiling distributed system models into practical implementations.