This repository is an experiment in trying to get AI to prove certain properties of distributed protocols. Specifically, the idea of communication closure.
Why? Because it is easier to test the protocols if they are communication closed.
The repo will prove in Lean for specific protocols - Raft and Paxos.