Mission

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 address the challenges posed by implementations of blockchain protocols. Our approach enables modular and scalable reasoning about composite systems, making verification efforts reusable and maintainable.

News

• [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.

Researchers

Core Team

• Ilya Sergey (PI), Yale-NUS College and NUS School of Computing
• Kiran Gopinathan, NUS School of Computing

Collaborators

• Prateek Saxena, NUS School of Computing
• George Pîrlea, Zilliqa Research

Related Publications

• Certifying Certainty and Uncertainty in Approximate Membership Query Structures
  Kiran Gopinathan and Ilya Sergey
  32nd International Conference on Computer-Aided Verification (CAV 2020)
  [PDF | Code]

• Safer Smart Contract Programming with Scilla
  Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan
  34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019)
  [PDF | Code]

• Towards Mechanising Probabilistic Properties of a Blockchain (Talk Abstract)
  Kiran Gopinathan and Ilya Sergey
  CoqPL 2019
  [PDF | Code]

• Distributed Protocol Combinators
  Kristoffer Just Andersen and Ilya Sergey
  21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019)
  [PDF | Code]

• Toychain: Formally Verified Blockchain Consensus
  George Pîrlea
  MEng Thesis, UCL, April 2019
  [PDF]

• Mechanising Blockchain Consensus
  George Pîrlea and Ilya Sergey
  7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)
  [PDF | Code]

• Programming and Proving with Distributed Protocols
  Ilya Sergey, James R. Wilcox, and Zachary Tatlock
  45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018)
  [PDF | Code]

Artefacts

GitHub Organisation

• Ceramist
  Verified hash-based AMQ structures in Coq
  Code on GitHub

• Toychain
  A Coq implementation of a minimalistic blockchain-based consensus protocol
  Code on GitHub

• Probchain
  Mechanised probabilistic properties of Nakamoto consensus
  Code on GitHub

• Disel
  A separation-style logic for compositional verification of distributed systems
  Code on GitHub