leanCL state transition in Lean 4, consensus rules verified by proof
Strawmap J* (2028~29) · leanCL STF in Lean 4
The state transition function, the core rule of leanCL, the next-generation consensus layer, is written in the proof tool Lean 4. The goal is to confirm the code is correct by mathematical proof rather than by tests.
Why it is needed
The consensus layer follows rules that turn the chain's state into the next state each time a block arrives. These rules are called the State Transition Function (STF). Today the rules are written as a Python spec, each client team reimplements them in its own language, and the implementations are then matched against the spec with tests. Tests only check the cases someone thought of in advance, so they cannot catch hidden contradictions in the spec or situations nobody imagined. leanCL is the next-generation consensus layer (lean consensus layer) that the Ethereum Foundation is researching. New components such as post-quantum signatures mean the rules have to be rewritten from scratch, and this item proposes writing the state transition function in Lean 4 when that happens. Lean 4 is both a programming language and a theorem prover. You write the code together with the properties it must satisfy as propositions, and a computer, not a person, checks that the proofs are correct. The lean in leanCL and the Lean in Lean 4 are an unrelated coincidence of the same word. This way the spec becomes a verified reference implementation, and mismatches in client implementations become easier to find. This is not a change to protocol rules but to how the spec and clients are built. The 2028 to 29 cell on the Strawmap is only an estimate, not a confirmed schedule.
How it works
- Write the rules in Lean 4 Write the state transition function, which takes a block and produces the next state, as Lean 4 code. This code serves as the official specification of the leanCL consensus rules.
- Write the required properties as propositions Properties such as "a finalized block is never reverted" and "a block containing an invalid signature is rejected" are written as mathematical propositions.
- The computer checks the proofs Lean 4 checks the proofs that the stated propositions actually hold for the code. A place where a proof fails signals a gap in the spec.