From Paper to Proof: How We Can Formally Verify Blockchain Protocols with Lean4

The security and correctness of blockchain protocols are guaranteed by numerous advanced mathematical theories, which are complex and require a significant amount of time to comprehend for most people. Although there are tons of papers and technical blogs that “prove” the security of those protocols in human’s natural language, there is no guarantee that those “manually-proved” proofs are correct. Unfortunately, humans are often misguided, and we frequently make incorrect claims (as evidenced by numerous examples of widely accepted mathematical results that were later proven to be false, as discussed in this mathoverflow thread).

One way to make the proof more reliable is to formally verify its correctness using automated theorem-proving systems, such as Coq and Lean4. Those tools allow us to formulate and verify mathematical proofs systematically, while their use itself is not easy to learn.

As an introductory tutorial, this post utilizes Lean4 to formally verify the consistency of the simple consensus protocol introduced in Professor Tim Roughgarden's great lecture at Columbia University. Although the assumption of this protocol is stronger than real situations, the following posts in this series aim to demonstrate the correctness of more practical protocols, such as Tendermint.

At the heart of every blockchain protocol lies a fundamental challenge: How can a group of distributed computers agree on a single sequence of transactions? This problem is solved by what’s known as a consensus mechanism.

To put it simply, blockchains function as shared global computers — master programs that coordinate all applications running on them, such as smart contracts. For this to work, all participating computers (called validators) must agree on the blockchain’s history: a chain of transactions that everyone accepts as the source of truth.

Let’s clarify some key terms:

• Validators are physical machines that run the blockchain protocol.
• Transactions are user-submitted actions, such as transferring tokens or executing contract logic.
• Blocks are ordered sequences of transactions.
• A chain is a sequence of blocks, forming the ledger history.

The role of a consensus mechanism is to ensure that all validators agree on a single chain of blocks. At each time step, validators:

• Perform local computations,
• Receive transactions from users and messages from other validators,
• Send messages to others to coordinate their views of the chain.

For simplicity, let’s begin with two basic assumptions:

1. Fixed validator set: The set of validators is predetermined and remains constant.
2. Synchronized time: All validators share a common notion of time, meaning they produce blocks at the same time intervals.

These assumptions simplify the design and analysis of consensus protocols.

There are two key properties that a consensus mechanism should satisfy:

• Consistency: All validators should agree on the same transaction history. In formal terms, the local chain of each validator must be a prefix of some single, agreed-upon global chain.
• Liveness: Every valid transaction submitted by a client will eventually be included in the blockchain. That is, progress is guaranteed.

Protocol A

Let’s start with the most basic idea for achieving consensus among validators.

At first glance, this protocol seems reasonable. However, it fails in more realistic network settings. For example, if the current leader crashes or experiences network delays, some validators may not receive the block in time. This leads to inconsistency in the validators’ local views of the chain.

Protocol B

To address the limitations of Protocol A, we now design Protocol B, a more resilient consensus mechanism that ensures consistency and liveness under the following assumptions:

• Crash Faults: Some validators may crash and stop participating permanently.
• Synchronous Network: Messages are delivered within a known delay bound ∆ (Delta).

Then, we propose the following mechanism:

In this blog post, we focus on why Protocol B guarantees consistency among all non-crashed validators.

We first show that at the end of every view v, the chains of all non-crashed validators are consistent, i.e., they are all prefixes of a single common chain. We use mathematical induction with respect to v.

Base Case (initial state):
All validators start with the same initial empty chain, so the claim holds trivially.

Inductive Step (view v):
Assume that at the beginning of viewv, the local chains of all non-crashed validators are consistent — they are all prefixes of a common chain.

• Each validator sends its chain Cᵢ to the leader ℓ. By the inductive hypothesis, all these Cᵢs are consistent.
• The leader selects the longest among them as C. Since all Cᵢs are consistent, C extend all of them.
• The new chain C* = (C, B) also extends all of them.
• Any validator that receives C* will update its local chain to C*, maintaining consistency.
• Even if some validators do not receive the new chain in time, their chains remain prefixes of C*, so consistency is preserved.

We then convert the above proof, written in human’s natural language, into a formal proof written in Lean4. We omit the detailed proofs of several lemmas for simplicity, but the complete code is available at https://github.com/Koukyosyumei/PoL.

We first model the basic components: block, chain, validator, and system. A block (Block) represented as a string (e.g., its hash). A chain (Chain) is a list of Blocks. Its current chain models a validator (Validator) and a flag indicating if it has crashed. A state of each view (StateB) consists of a list of validators and a designated leader.

We then define the single step of the Protocol B and the state at each time step as follows. In each view, the leader collects the chains of the validators, selects the longest chain, constructs new_chain by appending a new block to that chain, and sends new_chainto every non‐crashed validator. Here, we treat the leader's crash at each time step (is_leader_crashed_at_t) and the choice of the next leader at each time step (next_leader_at_t) as black boxes.

We then define the consistency of the system, which is the goal of our proof. Recall that two chains are consistent if one is a prefix of the other, and we define it as ChainsAreConsistent. This ensures there are no forks among the chains. Then, this system has the consistency property if the chains of any two non-crashed validators are consistent.

Given the above building blocks, our goal is to prove the following theorem: if the initial state is consistent, which holds trivially since all validators start with empty chains, then, at any time step t, the state evolved under Protocol B remains consistent, regardless of the choice of leader or when the leader crashes

Since this blog is a tutorial, we avoid relying heavily on automation and instead provide detailed, step-by-step proofs to make the explanations as straightforward as possible.

As we did in the proof in natural language, we use mathematical induction with respect to the time stamp t . When t = 0 , the goal is exactly the assumption h_initial_consistent .

We first define the abbreviation of key components:

Then, we use intro tactic as the pre-process:

As a consequence, our goal is transformed into the following:

We first prove three auxiliary lemmas. h_chains_consistent says that any pair of the old chain (chain of the time stamp t ) satisfies the consistency.

h_prefix says that for any non-crashed validator at the t+1 -th state, its chain is the prefix of the new chain at t+1 , where new_chain is the newly updated chain at the time stamp t .

h_nonupdate states that for any non-crashed validator at the t+1 -th state, if its chain is not equal to the new_chain , which means that the this validator couldn’t receive the new_chain at t , its chain belongs to the set of chains of the non-crashed validator at the t -th state.

Then, our final proof is as follows. This is somewhat redundant, so I encourage interested readers to optimize and shorten this proof. Since our goal is ChainsAreConsistent v1.chain v2.chain , we consider the four cases: whether v1.chain = new_chainand whether v2.chain = new_chain .

For example, when both are true, our proof proceeds as follows:

1. We first begin by unfold ChainsAreConsistent , whicn converts the goal into:

2. We focus on the left predicate by left tactic:

3. We rewrite v2.chain with new_chain based on h_c2_new :

4. We apply h_prefix (h_prefix : ∀ v ∈ state_tp1.validators, v.crashed = false → v.chain <+: new_chain), yielding two goals, which are trivially satisfied by the existing assumptions.

We can also finish the proofs of the other three cases with similar tactics.

In this post, we introduce the use of Lean4 to formally verify the consistency property of a simple blockchain consensus protocol. Although it may seem like a complicated task, it is worth learning and exploring the world of formal methods if you are dealing with mathematical properties that are directly related to millions of assets, such as blockchains. In the following post, we will also provide detailed tutorials on more realistic protocols and properties of blockchains with Lean4.