Aspects of concurrency and distribution pervasively appear in modern computing systems, including personal devices, data centers, aircrafts and medical devices. Due to complicated interactions between processes, concurrent and distributed systems are subtle and prone to bugs. Such bugs have led to death of patients and blackouts with millions of dollars financial loss. Can we build concurrent and distributed systems with static safety and security guarantees?

  In this talk, I present how we can exploit advances in formal methods to develop correct-by-construction concurrent and distributed systems. In particular, I show how proof techniques for specific classes of algorithms can simplify and automate the proof of correctness of those classes. First, I introduce a proof technique called condensability and a tool called Snowflake to verify linearizability of composing concurrent data-structures in Java. Snowflake generates proof obligations for condensability and discharges them using the Z3 SMT solver. Snowflake successfully verified a large fraction of composing methods in several open-source applications. Second, I present a framework in Coq called Chapar for development and modular verification of causally consistent replicated key-value store implementations and their clients. Chapar includes a novel proof technique for causal consistency of key-value store implementations that was used to verify two key-value store implementations from the literature. Extraction from Coq to OCaml resulted in two executable stores with the static causal consistency guarantee. Finally, I describe my future plans to build certified byzantine fault-tolerant replicated stores.