The goal of the CertiChain project is to develop a framework for computer-aided verification of correctness properties of blockchain-based distributed consensus protocols: their safety, liveness, and probabilistic security guarantees. We build on the recent advances in applying mechanised interactive theorem proving for establishing machine-checked correctness of safety-critical distributed systems. We employ the state-of-the-art techniques from foundational formal verification to distributed systems to add
[6 Apr 2020] The work on the Ceramist framework has been accepted to CAV 2020 .
[17 Sep 2019] The project has been funded by NSOE-TSS program.