EVEREST: Nearly full automatic verification for geo-replicated systems

Distributed systems commonly replicate data to improve the system’s overall availability, scalability,
and fault tolerance. However, replication increases the complexity of the system as keeping replicas
consistent is a difficult task. As a result of the CAP theorem, much work has focused on programming
abstractions/models for ensuring strong consistency (e.g., distributed consensus) or eventual
consistency (e.g., replicated data types). To ensure the correctness of such abstractions, researchers
rely on a formal specification with manual paper proof. Recently, frameworks have been proposed to
verify correctness properties using proof assistants. Those frameworks, however, use abstract
specifications that are disconnected from actual implementations and require significant expertise to
be used properly.
To simplify the development of geo-replicated systems, we take a radical new approach to reduce the
programming effort and expertise needed to verify the correctness of distributed abstractions for
replicated state. We aim to explore a high-level language that offers constructs that can be
automatically verified by supporting transpilation to an SMT language. We will explore support to
derive user-defined metadata (e.g., assumptions) to optimize and steer verification when full
automation is not possible, e.g., for recursive data structures. Our approach has the potential to
fundamentally developers build correct abstractions without requiring separate specifications