A Framework for Formally Verifying Blockchain Consensus

Funder	Engineering and Physical Sciences Research Council
Recipient Organization	Imperial College London
Country	United Kingdom
Start Date	Sep 30, 2024
End Date	Mar 30, 2028
Duration	1,277 days
Number of Grantees	1
Roles	Supervisor
Data Source	UKRI Gateway to Research
Grant ID	`2929229`

Grant Description

The aim of this research is to develop a framework that can be used to model and verify blockchain consensus protocols. This framework would be formalised as a calculus in a theorem prover. To achieve the aim of this project, we break it down into the following objectives: 1. Develop a Language for the specification of a blockchain network and its consensus

protocol. 2. Using the language, develop a calculus to verify such protocols and implement it in the chosen theorem prover. 3. Using the calculus, prove general properties of a blockchain network and consensus protocols to complete the framework. 4. Instantiate the framework for a specific blockchain or consensus protocol.

Blockchain and verification