Remember, two years ago James Wilcox and Doug Woos were formally proving Raft's linearizable semantics using Verdi: https://news.ycombinator.com/item?id=10017549
> Both the Verdi framework and our verified Raft implementation are open-source. Please feel free to submit comments, issues, and pull requests on either repository.