Mechanising blockchain consensus
Abstract
We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant.
DOI 10.1145/3167086
Related papers
- Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts OOPSLA 2023
- Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction ECOOP 2025
- Quorum Tree Abstractions of Consensus Protocols ESOP 2023
- LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols PLDI 2025
- LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs PLDI 2024
- Formal verification of authenticated, append-only skip lists in Agda CPP 2021
- Safer smart contract programming with Scilla OOPSLA 2019
- SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols PLDI 2026