George Pirlea, Ilya Sergey (University College London, UK)
Also Karl Palmskog in development
Master thesis of George Pîrlea
The protocol’s executions are modeled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated.
Karl Palmskog et.al.
Quiescent consistency (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
Sebastian Burckhardt (Microsoft Research), et al.
Douglas B. Terry et. al. by Xerox Palo Alto Research Center
cited by more than 1000 papers
no in-flight instances only of BlockMsg
a clique network topology for simplicity
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
Kiran Gopinathan (University College London, UK), Ilya Sergey (Yale-NUS College and School of Computing, NUS, Singapore)
Bitcoin Backbone Protocol in Coq
Built on libraries by Affeldt and Hagiwara, which provides a probability framework implemented on top of the Ssreflect extension for Coq