As the authors note, “despite the hype about blockchains and distributed ledgers, no formal abstraction of these objects has been proposed.” Maurice Herlihy also observed this in his 2017 keynote talk [1]. This paper makes a start in that direction, by defining a model of a distributed ledger object--a sequence of items--and the properties to be expected from such a system. These properties are then proved for a selection of distributed realizations of the model in which certain consistency guarantees can be delivered.

The paper presents solid results in support of the enterprise of formalization in this area, but fails to deliver as strong a contribution as might be expected. First, the formalization is entirely informal rather than having any formal machine support. It is therefore difficult to assess the presented results, particularly when only sketches of proofs are available. It would have been reassuring to see a formalization of the models, implementations, and results in a proof assistant, such as Coq or Isabelle, because this formalization could weed out any typographical errors or more subtle bugs in the specification and results.

Second, the results don’t really apply to existing blockchains such as Bitcoin, whose consistency guarantees are given probabilistically. Some results on these consensus protocols are available in the literature, and it would be good to see them explored in any follow-up to the work reported here.