Paper 2020/917

Formalizing Nakamoto-Style Proof of Stake

Søren Eller Thomsen and Bas Spitters


Fault-tolerant distributed systems move the trust in a single party to a majority of parties participating in the protocol. This makes blockchain based crypto-currencies possible: they allow parties to agree on a total order of transactions without a trusted third party. To trust a distributed system, the security of the protocol and the correctness of the implementation must be indisputable. We present the first machine checked proof that guarantees both safety and liveness for a consensus algorithm. We verify a Proof of Stake (PoS) Nakamoto-style blockchain (NSB) protocol, using the foundational proof assistant Coq. In particular, we consider a PoS NSB in a synchronous network with a static set of corrupted parties. We define execution semantics for this setting and prove chain growth, chain quality, and common prefix which together implies both safety and liveness.

Available format(s)
Publication info
Preprint. MINOR revision.
blockchainformal methods
Contact author(s)
sethomsen @ cs au dk
spitters @ cs au dk
2021-06-11: revised
2020-07-26: received
See all versions
Short URL
Creative Commons Attribution


      author = {Søren Eller Thomsen and Bas Spitters},
      title = {Formalizing Nakamoto-Style Proof of Stake},
      howpublished = {Cryptology ePrint Archive, Paper 2020/917},
      year = {2020},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.