Stream: Coq users

Topic: More Coq and distributed consensus


view this post on Zulip Karl Palmskog (Aug 21 2020 at 13:37):

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.

view this post on Zulip Bas Spitters (Aug 21 2020 at 13:52):

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

view this post on Zulip Karl Palmskog (Aug 21 2020 at 13:57):

they claim they are "truly asynchronous BFT", not sure exactly how this should be interpreted

view this post on Zulip Karl Palmskog (Aug 21 2020 at 14:01):

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)

view this post on Zulip Karl Palmskog (Aug 21 2020 at 14:02):

some slides here: https://www.cylab.cmu.edu/_files/documents/formal-methods-3-kcrary-formalizing-the-hashgraph-gossip-protocol.pdf

view this post on Zulip Bas Spitters (Aug 21 2020 at 14:23):

So seems to be in the flavor of Velasarios: BFT, safety, no liveness.

view this post on Zulip Karl Palmskog (Aug 23 2020 at 17:35):

and yet another: https://github.com/novifinancial/LibraChain

view this post on Zulip Bas Spitters (Aug 23 2020 at 18:50):

Francois spoke at TPBC. I believe the developments has similar limitations as toychain, on which it is based.

view this post on Zulip Karl Palmskog (Oct 06 2020 at 21:07):

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