Karl Palmskog (Aug 21 2020 at 13:37): 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.
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
Karl Palmskog (Aug 21 2020 at 13:57):they claim they are "truly asynchronous BFT", not sure exactly how this should be interpreted
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)
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
Bas Spitters (Aug 21 2020 at 14:23):So seems to be in the flavor of Velasarios: BFT, safety, no liveness.
Karl Palmskog (Aug 23 2020 at 17:35):and yet another: https://github.com/novifinancial/LibraChain
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.
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: Oct 13 2024 at 01:02 UTC