Distributed data stores are expected to stay consistent and often available and responsive even in the face of site crashes and network partitions.  Therefore, distributed algorithms are challenging to design and understand, and distributed-system bugs are notoriously hard to find and reproduce.  Yet many social, infrastructural, and governmental services are dependent on distributed stores.  The reliability of applications can be enhanced by precise specification of consistency and liveness properties and verification techniques that prove the compliance of the store implementations with the specification.  The mission of this project is to build certified distributed stores i.e. stores whose proof of safety, liveness and security guarantees are mechanically checked using the modern proof assistants, before the system is deployed.  The project encompasses the following interdependent aspects: design and specification of safety and liveness criteria, verification methods and tools for distributed stores, and verification and testing tools for client programs. 

There are diverse industrial distributed stores that provide a spectrum of weak to strong notions of consistency. Our first efforts have resulted in causally consistency distributed key-value stores that are verified in Coq and run using OCaml.  For our next step, we target transactional distributed stores.