Mechanising Blockchain Consensus
(University College London, UK)
Also Karl Palmskog in development
Toychain: Formally Verified Blockchain Consensus
Master thesis of George Pîrlea
Reasoning about Byzantine Protocols (slide)
The protocol’s executions are modeled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated.
Casper FFG extention
Formal verification of Hybrid Casper FFG
Karl Palmskog et.al.
(on blocks, not transactions)
"when there are no inflight messages between any of the nodes, they all should agree on the local ledger, which can be, thus, thought of as a globally shared one"
citing these paper
Replicated Data Types: Specification, Verification, Optimality
Sebastian Burckhardt (Microsoft Research), et al.
Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System
Douglas B. Terry et. al. by Xerox Palo Alto Research Center
cited by more than 1000 papers
no in-flight instances only of
a clique network topology
restricting the initial configurations to those where every node’s known peers include all addresses in the global state.
no "late joiners"
inductive for systems that start in initial configurations with a clique network topology
no crash faults nor byzantine faults
Theorem 5.1 (Consensus in a clique topology).
For 𝜎 = ⟨∆, 𝑃⟩, if Cliq(𝜎) holds, then there exists a chain 𝑐, such that for any node 𝑎 ∈ dom(𝜎), 𝑐 ≥ ledger (∆, 𝑎) and blocksFor (𝑃, 𝑎) = ∅ implies ledger (∆, 𝑎) = c
Towards Mechanising Probabilistic Properties of a Blockchain
Kiran Gopinathan (University College London, UK), Ilya Sergey (Yale-NUS College and School of Computing, NUS, Singapore)
Bitcoin Backbone Protocol
Built on libraries by
Affeldt and Hagiwara
, which provides a probability framework implemented on top of the Ssreflect extension for Coq