I had somehow missed this work by Karl Crary at CMU(!) on formalizing a distributed consensus algorithm: https://www.cs.cmu.edu/~crary/papers/2018/hashgraph-v2.tgz https://medium.com/hashgraph/coq-proof-completed-by-carnegie-mellon-professor-confirms-hashgraph-consensus-algorithm-is-abft-1467cc4de3d8
@Bas Spitters apparently our fates are seemingly to study type theory, then to prove blockchains correct forever
Or maybe, blockchain verification is the price of any kind of proliferation of type theory systems.
It's still unpublished: https://www.cs.cmu.edu/~crary/papers/
How does it fit in our comparison table on p5. I understand it is PBT (not Nakomoto). Does he prove safety and liveness under reasonable conditions?
they claim they are "truly asynchronous BFT", not sure exactly how this should be interpreted
very cursory inspection of Coq code gives that there is a proof along the lines of: there is the possibility of consensus (and if it happens it's correct)
some slides here: https://www.cylab.cmu.edu/_files/documents/formal-methods-3-kcrary-formalizing-the-hashgraph-gossip-protocol.pdf
So seems to be in the flavor of Velasarios: BFT, safety, no liveness.
and yet another: https://github.com/novifinancial/LibraChain
Francois spoke at TPBC. I believe the developments has similar limitations as toychain, on which it is based.
One more addition to the quickly-growing collection of Coq consensus protocol formalizations: https://github.com/runtimeverification/giskard-verification (I was not the primary author of this one, which may explain absence of MathComp.)
Last updated: Jan 29 2023 at 01:02 UTC