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.
- [17 Sep 2019] The project has been funded by NSOE-TSS program.
- Ilya Sergey (PI), Yale-NUS College and NUS School of Computing
- Kiran Gopinathan, NUS School of Computing
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]
Toychain: Formally Verified Blockchain Consensus
MEng Thesis, UCL, April 2019