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.
