This (WIP) repository contains formal specs & proofs of distributed systems concepts, including consensus protocols, foundational definitions & conjectures, as well as impossibility results.
All specifications & proofs are written using the Athena language.
The first example (and only one currently filled in) is called "Simple Agreement". This is a quite simple consensus protocol based on the one used by Martin Kleppmann in his case study / tutorial titled "Verifying distributed systems with Isabelle/HOL". The code files for Kleppmann's Isabelle/HOL formalization can be found in the following gist: Correctness proofs of distributed systems with Isabelle.
More examples are to come (including: a p2p gossip protocol that uses randomness to select subset of neighbors, as well as Paxos, Dolev-Strong, and Tendermint). This repository also specifies some abstract modules that include definitions and theorems meant to be reused across theories such as the abstract specifications of Byzantine Broadcast & State Machine Replication.
- Progress
- Simple Agreement
- Paxos
- Dolev-Strong
- P2P Gossip