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?

https://arxiv.org/abs/2007.12105

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: Sep 23 2023 at 08:01 UTC