Etheorem update: the complete executable consensus specs written in Lean 4

Дата публикации: 21-09-2026 12:51:22

In May this year we started working on Etheorem, the complete executable consensus specs in Lean 4
This post is an update of the state of the project. The Lean 4 specification pass all the pyspec vectors for the state transition, the fork choice, and the containers we model, on three forks, Fulu, Gloas and Heze. This include the two presets, mainnet and minimal.
In this post we explain the stack, the framework, and how the specs look. We also show how the framework make the proofs easy to state.
The stack
The project is a monorepo of packages. It organizes as a stack:
Fulu spec Gloas spec Heze spec
Fulu proofs Gloas proofs Heze proofs
─────────────────────────────────────────────────
EthCLLib
(the consensus spec framework)
─────────────────────────────────────────────────
SizzLean
(SSZ, machine-checked proofs)
─────────────────────────────────────────────────
LeanSha256 (pure) · LeanHazmat (FFI bridges: BLS, KZG, native SHA-256)
Every fork of the top layer has two parts at the same level, the executable implementation of the spec and the proofs about the spec. Both read from the same definitions. The framework package is EthCLLib, the fork bodies live in a sibling package, EthCLSpecs, that is the namespace you see in the code.
SizzLean: the SSZ base
We explained SizzLean in the previous post (Lean4 SSZ library: formally verified and easy to use), we will not repeat it here. In short: it is, how far as we know, the first SSZ library in Lean 4, and today it is the only one public that runs under a Lean 4 rendering of the consensus state transition and fork choice. The serialization, the deserialization and the Merkleization carry machine-checked proofs of the central properties, and it pass the full upstream conformance corpus. In the stack above it is the bottom layer, every container of the consensus spec serializes and hashes through it.
EthCLLib: the framework
EthCLLib gives the authoring surface for defining forms, containers, functions, constants/presets amd the inheritance system between forks, so only what changes in that fork has to be written.
This is the heart of the code. EthCLLib and the interface with the other layers has been carefully handcrafted, and this have been documented extensively in markdown so AI agents can follow the architecture without problems.
This is mainly in three documents:
The Spec-Authoring Model
The Framework Architecture
The Specs Architecture
Defining a container. A container is a field list, and a field can size itself by preset constants:
forkcontainer Attestation where
aggregationBits : Bitlist (Const.maxValidatorsPerCommittee * Const.maxCommitteesPerSlot)
data : AttestationData
signature : BLSSignature
committeeBits : Bitvector Const.maxCommitteesPerSlot
The capacity bounds are symbolic, they resolve through the fork’s Const tier at instantiation. One declaration elaborates into a structure parameterized over [Preset], with the SSZ instances derived per preset, mainnet and minimal. The functions over it are written once, sszGet attestation aggregationBits, and run at both presets unchanged. The conformance runs show this for example, the same ssz_static code pass at mainnet and minimal.
Defining a function. Every spec function is a forkdef definition. The section header creates the genericity plumbing, is generated by a macro, the author never writes it:
state_section
forkdef processSlashingsReset : StateTransition Unit := do
…
Defining a constant. The constants live in a Const tier per fork. Some come from the preset, some are the fork’s own:
forkabbrev ptcSize : Nat := Preset.ptcSize
forkabbrev builderWithdrawalPrefix : UInt8 := 0x03
ptcSize reads the Gloas preset, so mainnet and minimal take their own values. builderWithdrawalPrefix is a plain constant of the fork.
Inheritance between forks. A fork declares its inheritance in one line:
import EthCLSpecs.Fulu
namespace EthCLSpecs.Gloas
fork Gloas from Fulu
end EthCLSpecs.Gloas
Every form above is captured at declaration time for per-fork replay. The parent’s declarations can be inherited or overrided, also new declarations can be added. Use inherit macro to inherit, a declaration of the same name is an override, a fresh name is new declaration in that fork. This applies to containers, functions and constants.
inherit Checkpoint
inherit Attestation
inherit Validator
-- the full list is one file, Gloas/Inherited.lean
The constants inherit the same way, inherit slotsPerEpoch maxCommitteesPerSlot …, one explicit line per name in the fork’s constants file. The type vocabulary too, inherit Slot Gwei Root … in the types file, replayed as this fork’s own aliases.
For functions, the part that makes it work is late binding: an inherited body re-elaborates in the child namespace, so every name inside resolves to the child’s own containers, constants and overrides:
-- Gloas/Transition.lean: the block steps EIP-7732 leaves unchanged
inherit processRandao
inherit processEth1Data
inherit verifyBlockSignature
-- the steps the EIP touches, overridden, callees bind to Gloas's own
forkdef processOperations (body : BeaconBlockBody) : StateTransition Unit := do
…
processRandao arrives in Gloas operating over Gloas state, and a call it makes to an overridden function resolves to the Gloas version.
If a fork body names a container it did not inherit fails to elaborate. The fork body names only its own namespace plus the framework, there is no open into the parent fork. On the function surface the numbers are: Fulu (which includes everything since phase0) declares 158 spec functions, Gloas adds 109 of its own and re-elaborates the rest through inheritance, Heze adds 12 on top of Gloas.
Generic on the things a spec should not care about. A spec body is generic over the effect monad, the hash function, the Merkle cache and the finite-map backend. The same source elaborates into two configurations:
Axis
fast (test runner)
pure (proofs)
Effect monad
EStateM
StateT State (Except _)
Hasher
SHA-256 over FFI
pure-Lean SHA-256, kernel-reducible
Merkle box
cached tree
uncached
Fork-choice map
hashMap
treeMap
BLS crypto
blst over FFI, behind a signature cache
symbolic, a signature check is assumed true
The BLS backend is a parameter the same way. The proofs inject the symbolic backend, so a transition theorem carries no crypto in its trust base.
The author can write the spec as generic of all these. The test runner instantiates the fast column, the proofs instantiate the pure column, the one that reduces in the kernel. The hash function stays a parameter too, so if there is future swap the spec functions and the proofs stay.
The state transition and the store transition are monadic. Every step of the spec is a value of type StateTransition Unit, a program in a state monad. The monad connect the state, so a step reads as a sequence of actions, the state passing stays out of the way:
forkdef weighJustificationAndFinalization (totalActive prevTarget currTarget : Gwei) :
StateTransition Unit := do
let state ← get
let prevEpoch := previousEpochOf state
…
modifyState fun state => …
The same shape holds in fork choice. The store is a second machine, a store transition, and the framework runs the state transition nested inside it. One definition of the state transition serves both, the spec writes it once. This design helps in three ways:
Errors live in the monad. A step that finds an invalid condition rejects, and the monad short-circuits. The fast column carries the post state on the reject, that is how the runner matches the Python, that mutates in place and catches the expected raise. The pure configuration returns the error alone, a rejected run leaves no half-written state behind, and the theorems stay about values.
The step is generic over the monad, this is the first row of the table above. Write the step one time, run it fast, prove it pure.
A proof about a step is an equation about its run. Running a bind is running the first action and, on success, the continuation from the value and state it produced. Running pure is the value paired with the state, unchanged. This allows composability of proofs.
process_epoch shows where this pays. The Python:
def process_epoch(state: BeaconState) -> None:
process_justification_and_finalization(state)
process_inactivity_updates(state)
process_rewards_and_penalties(state)
process_registry_updates(state)
process_slashings(state)
process_eth1_data_reset(state)
process_pending_deposits(state)
process_pending_consolidations(state)
process_effective_balance_updates(state)
process_slashings_reset(state)
process_randao_mixes_reset(state)
process_historical_summaries_update(state)
process_participation_flag_updates(state)
process_sync_committee_updates(state)
# [New in Fulu:EIP7917]
process_proposer_lookahead(state)
Etheorem:
/-- `process_epoch` (Fulu ordering). -/
forkdef processEpoch : StateTransition Unit := do
processJustificationAndFinalization
processInactivityUpdates
processRewardsAndPenalties
processRegistryUpdates
processSlashings
processEth1DataReset
processPendingDeposits
processPendingConsolidations
processEffectiveBalanceUpdates
processSlashingsReset
processRandaoMixesReset
processHistoricalSummariesUpdate
processParticipationFlagUpdates
processSyncCommitteeUpdates
processProposerLookahead
The two list the same fifteen substeps, in the same order, the Fulu ordering. The difference is the state. In the Python every line passes state by hand, fifteen times, and each substep mutates it in place, so the state flow is a convention the reader carries in the head. In the Lean the monad carries the state, every line is just the step, and the sequencing is the do block itself. The same fifteen steps run in the runner through the fast configuration, and in the proofs through the pure configuration, where the two run equations turn the block into a chain of equations, one per substep.
process_operations makes the same point at the next level, where the steps become handlers over a block body. The Python:
def process_operations(state: BeaconState, body: BeaconBlockBody) -> None:
# Disable former deposit mechanism once all prior deposits are processed
eth1_deposit_index_limit = min(
state.eth1_data.deposit_count, state.deposit_requests_start_index
)
if state.eth1_deposit_index < eth1_deposit_index_limit:
assert len(body.deposits) == min(
MAX_DEPOSITS, eth1_deposit_index_limit - state.eth1_deposit_index
)
else:
assert len(body.deposits) == 0
def for_ops(operations, fn) -> None:
for operation in operations:
fn(state, operation)
for_ops(body.proposer_slashings, process_proposer_slashing)
for_ops(body.attester_slashings, process_attester_slashing)
for_ops(body.attestations, process_attestation)
for_ops(body.deposits, process_deposit)
for_ops(body.voluntary_exits, process_voluntary_exit)
for_ops(body.bls_to_execution_changes, process_bls_to_execution_change)
for_ops(body.execution_requests.deposits, process_deposit_request)
for_ops(body.execution_requests.withdrawals, process_withdrawal_request)
for_ops(body.execution_requests.consolidations, process_consolidation_request)
Etheorem:
forkdef processOperations (body : BeaconBlockBody) : StateTransition Unit := do
let state ← get
let limit := umin (sszGet state eth1Data).depositCount (sszGet state depositRequestsStartIndex)
if (sszGet state eth1DepositIndex) < limit then
assert (UInt64.ofNat body.deposits.size == umin (UInt64.ofNat Const.maxDeposits) (limit - (sszGet state eth1DepositIndex)))
else
assert (body.deposits.size == 0)
for op in body.proposerSlashings do processProposerSlashing op
for op in body.attesterSlashings do processAttesterSlashing op
for op in body.attestations do processAttestation op
for op in body.deposits do processDeposit op
for op in body.voluntaryExits do processVoluntaryExit op
for op in body.blsToExecutionChanges do processBlsToExecutionChange op
for op in body.executionRequests.deposits do processDepositRequest op
for op in body.executionRequests.withdrawals do processWithdrawalRequest op
for op in body.executionRequests.consolidations do processConsolidationRequest op
The deposit condition reads almost the same in both. The difference sits in the dispatch. In the Python every handler takes (state, operation) and mutates, so a helper is needed, one that closes over the local state and passes it by hand. In the Lean every handler is already a step of the same monad, so the dispatcher is direct sequencing, for op in … do handler op, and the state never appears because the monad carries it.
This is also where the proofs enter. process_epoch showed a chain of substeps, process_operations is a chain of handlers, and both reduce the same way: the run equation of the whole is the composition of the run equations of the pieces. Each handler can be characterized in isolation, its own proposition and the dispatcher’s theorem chains them.
The specs: Fulu, Gloas and Heze
The result first. The Lean specs pass:
the state-transition vectors of the three forks, at mainnet and minimal,
the fork-choice vectors of the three forks, at both presets,
the ssz_static container vectors for every container the spec models, at both presets,
pinned at consensus-spec-tests v1.7.0-alpha.11. A few container families the spec does not model yet, the light-client and gossip-aggregation types among them, xfail as out of scope, we prefer an honest xfail over a silent gap. On the SSZ layer, the ssz_generic wire-format suite pass complete, 2215 cases, pinned at v1.7.0-alpha.13, the last release that carries those vectors. Conformance here is behavioral: a fork is correct when it pass the upstream vectors, the same bar a client team use.
Readability. Our goal is that the Lean reads as close to the spec as possible. A small example, picked on purpose for its size. The Python of decrease_balance:
def decrease_balance(state: BeaconState, index: ValidatorIndex, delta: Gwei) -> None:
"""
Decrease the balance of a validator or 0 Gwei floor.
"""
balance = state.balances[index]
state.balances[index] = balance - delta if balance >= delta else 0
Etheorem:
forkdef decreaseBalance (state : State) (i : ValidatorIndex) (delta : Gwei) : State :=
modBalance state i (fun balance => if delta > balance then 0 else balance - delta)
Two differences to notice, not criticism to the Python, which is the reference code. The Lean version returns the new state, nothing mutates in place. The monad connects the state underneath and the proofs use the configuration that reduces in the kernel. And the field paths are checked at compile time where in the Python it is at run time.
In some cases the Lean reads better than the Python. The named-field update macro makes the checkpoint bookkeeping readable, each branch says what it justify and what bit it set:
state := sszUpdate state with
currentJustifiedCheckpoint := { epoch := prevEpoch, root := prevRoot },
justificationBits := bitSet (sszGet state justificationBits) 1 true
The same for process_voluntary_exit in python:
def process_voluntary_exit(state: BeaconState, signed_voluntary_exit: SignedVoluntaryExit) -> None:
voluntary_exit = signed_voluntary_exit.message
validator = state.validators[voluntary_exit.validator_index]
# Verify the validator is active
assert is_active_validator(validator, get_current_epoch(state))
# Verify exit has not been initiated
assert validator.exit_epoch == FAR_FUTURE_EPOCH
# Exits must specify an epoch when they become valid; they are not valid before then
assert get_current_epoch(state) >= voluntary_exit.epoch
# Verify the validator has been active long enough
assert get_current_epoch(state) >= validator.activation_epoch + SHARD_COMMITTEE_PERIOD
# [New in Electra:EIP7251]
# Only exit validator if it has no pending withdrawals in the queue
assert get_pending_balance_to_withdraw(state, voluntary_exit.validator_index) == 0
# signature verification and exit initiation follow
Etheorem:
forkdef processVoluntaryExit (sve : SignedVoluntaryExit) : StateTransition Unit := do
let state ← get
let ve := sve.message
let hb ← assertH (ve.validatorIndex.toNat < (sszGet state validators).size)
let validator := (sszGet state validators)[ve.validatorIndex.toNat]'hb.down
assert (isActiveValidator validator (currentEpochOf state))
assert (hasNotInitiatedExit validator)
assert (currentEpochOf state ≥ ve.epoch)
assert (passedShardCommitteePeriod validator (currentEpochOf state))
assert (getPendingBalanceToWithdraw state ve.validatorIndex == 0)
The function reads line for line, each check is a named predicate of the fork’s vocabulary, hasNotInitiatedExit instead of the raw exit_epoch == FAR_FUTURE_EPOCH comparison, passedShardCommitteePeriod instead of the epoch arithmetic. And the one check about a bound, the validator index in range, uses assertH, it returns the bound it just proved and the next line consumes it, so the indexing is total.
We say “in some cases” because the general case is still open. Some parts, as the delta loops of the rewards, are more readable in the Python today, and making the Lean readable in general is a direction of the project. On performance we say little on purpose: today the target of the fast configuration is conformance at mainnet state scale, the target of the project is a spec you can prove things about, a client is a different artifact.
The proofs
Because the spec bodies are generic, the framework let us state theorems about them and instantiate them at the pure configuration. A proof starts by the proposition and we try to make the proposition readable. Example, a characterization of the Gloas predicate that says if a builder can cover its bid:
@[characterizes EthCLSpecs.Gloas.canBuilderCoverBid]
theorem canBuilderCoverBid_iff [Preset] [HasherTag] :
∀ (state : Gloas.State) (builderIndex : BuilderIndex) (bidAmount : Gwei),
canBuilderCoverBid state builderIndex bidAmount = true ↔
let builderBalance := (sszGet state builders[builderIndex.toNat]!).balance
let minBalance :=
Gloas.Const.minDepositAmountG +
getPendingBalanceToWithdrawForBuilder state builderIndex
minBalance ≤ builderBalance ∧ bidAmount ≤ builderBalance - minBalance
Step by step, the proposition says:
for every state, builder index and bid amount, ∀ (state : …) …,
the function returns true exactly when (↔, an if-and-only-if),
the minimum balance, the deposit amount plus what is locked pending withdrawal, does not exceed the builder balance, minBalance ≤ builderBalance,
and the bid fits in what remains, bidAmount ≤ builderBalance - minBalance.
The proofs of these propositions are generated with AI assistance. But the Lean kernel check every proof independently of who or what wrote it, and the repo publishes the coverage table and the axiom inventory, so the trust base is auditable, #print axioms lists everything a theorem rests on.
Where does this stand today? 8 spec functions are fully characterized, 29 more appear in theorem statements, of 585 in the three forks. It is early. The repo tracks it in a proof ledger. Appendix A lists the consensus-specs proofs currently, Appendix B is the SSZ table. The SSZ layer below is in a more advanced state, see the previous post.
The team
Etheorem is built by a team of seven, with contributors from the Ethereum Protocol Fellowship and the Invisible Garden Fellowship: Mouzayan, irajgill, IvanAnishchuk, protocolwhisper, Sahilgill24, adria0, and leolara. Thanks to their hard work, and special thanks to Mouzayan and IvanAnishchuk, who wrote most of the fork-spec proofs, including the theorem we show above, and to irajgill, who wrote many of the SSZ proofs.
In the philosophy of Invisible Garden, one aspect of this project is learning. We were not formal verification experts previously, we are learning it by doing, the previous post told that story. People are welcome to join and co-learn. There are concrete doors to enter: the proof ledger has one row per candidate function and some rows are still open, pick one and characterize it, or take a spec function you know well and review a row. Any review, feedback, contribution and of course, use is welcomed.
Feedback welcome
The repo is github.com/etheorem/etheorem, the status page of each package records what is proved and what is not.
Questions for the readers: which spec function would you want to see characterized first?
Appendix A: the consensus-specs proofs, function by function
The proved rows of the ledger, theorem by theorem. All names live under EthCLSpecs.Proofs.Gloas unless noted. Every theorem is checked by the Lean kernel, and the axiom footprint of the whole set is the three standard kernel axioms, propext, Classical.choice, Quot.sound, nothing else: no crypto, no compiler trust, no reduction axioms, the symbolic BLS backend keeps signature checks out of the trust base.
Spec function
Theorems
What they establish
toBuilderIndex, convertBuilderIndexToValidatorIndex
toBuilderIndex_convertBuilderIndexToValidatorIndex, convertBuilderIndexToValidatorIndex_toBuilderIndex, isBuilderIndex_convertBuilderIndexToValidatorIndex
the flag round trip, both directions is the identity, and the flag bit is exactly the builder tag
canBuilderCoverBid
canBuilderCoverBid_iff, canBuilderCoverBid_iff_toNat_add_le
returns true exactly when the minimum balance fits and the bid fits in the remainder, in UInt64 form and restated over Nat
initiateBuilderExit
initiateBuilderExit_run_eq, …_run_builders, …_run_inRange, …_run_outOfRange, …_run_inRange_no_wrap, plus unconditional minimal and mainnet corollaries
the exact whole-transition equation, the registry effect at every index, never rejects in or out of range, the withdrawable epoch never wraps
processBuilderPendingPayments
processBuilderPendingPayments_run, expectedPaymentWindow_get_lt, expectedPaymentWindow_get_upper, …_run_of_fits
the two-field successful-run postcondition, the payment window entries on both halves of the window, capacity-guarded corollary
isValidIndexedPayloadAttestation
isValidIndexedPayloadAttestation_eq_true_iff
accepts exactly the non-empty, adjacent-nondecreasing, in-range committee index sets, backend-generic
updateCheckpoints
updateCheckpoints_eq, …_justifiedCheckpoint_eq_or_advances, …_finalizedCheckpoint_eq_or_advances, …_justifiedEpoch_le, …_finalizedEpoch_le
the single record update equation, each checkpoint equal or advancing, the store epochs never lowered
processOperations
processOperations_eq_seq, processOperations_nonempty_deposits_error
the coordinator equation, the deposit-count check then the six family folds in order, non-empty in-block deposits reject there
initializePtcWindow
initializePtcWindow_lt, …_ge, …_lt_default
the window’s regions, entry by entry, with the placeholder default
getPtc
getPtcElseOffset_lt_next_slot, getPtcElseOffset_lt_same_slot
the unchecked offset precondition holds at the guarded call sites, in progress
Beyond the per-function rows:
ForkChoiceRun carries the run-equation machinery into fork choice: a fork-choice forkdef at the pure store monad satisfies the same kind of run facts, and a state-transition theorem crosses over by function application.
On the framework side, EthCLLib.Proofs.MerkleBranch proves isValidMerkleBranch_iff: the branch check is exactly a reconstruction, an honest opening of a SizzLean tree passes it, the branch fold equals the tree’s own opening.
Heze has two rows in progress, shouldExtendPayload and recordPayloadInclusionListSatisfaction, the FOCIL enforcement chain.
Fulu has 2 spec functions touched by theorem statements, Heze 6, Gloas 21, of the 585 total.
Appendix B: the SizzLean proofs
The three central theorems hold on the BasicSupported cut of the SSZType universe, under the value-level guard EncodedFits s x, the encoded size below MAX_LENGTH. Per constructor:
SSZType constructor
decode_encode
serialize_injective
encode_size_le_max
Technique
.uintN 8
closes by rfl after one unfold
.uintN 16
Nat-digit codec, Proofs/UInt.lean
.uintN 32
Nat-digit codec, Proofs/UInt.lean
.uintN 64
Nat-digit codec, Proofs/UInt.lean
.uintN 128
Nat-digit induction on the little-endian codec
.uintN 256
same codec proof as .uintN 128
.bool
exhaustive cases + rfl
.vector t n, fixed-size t
recurses on the element type’s witness
.vector t n, variable-size t
offset-table codec, Proofs/CollectionVar.lean
.list t cap, fixed-size t
recurses on the element type’s witness
.list t cap, variable-size t
offset-table codec, empty list is the empty buffer
.bitvector n
byte-level bit-packing inverse, Proofs/BitPack.lean
.bitlist cap
bit-packing inverse + length-marker recovery
.container fs, all fields fixed
mutual recursion on the field list
.container fs, mixed fixed/variable
offset-table codec
The bit arms close by kernel decide over the finite chunk shapes and add no axioms beyond the standard three.
On Merkleization, proved today: the cached tree’s agreement with the spec merkleization for every BasicSupported arm, per shape and up to a fresh box’s hashTreeRoot, the path-bit round trips, the openings, the generalized-index model, and branch completeness, which is what the Merkle branch theorem of Appendix A builds on. The cached tree beyond the fresh box, the update path, is the execution path today, checked by the test suites, the coherence and builder theorems in the repo are the seed of the future equivalence theorem. Row-level status lives in the SizzLean proof ledger.
decode_encode and serialize_injective rest only on the three standard kernel axioms, encode_size_le_max adds none.
Leo Lara

Схожие новости

#	Наименование новости	Тональность	Информативность	Дата публикации
1	Lean4 SSZ library: formally verified and easy to use	0	13.53	13-09-2026
2	Scaling Ethereum with recursive STARKs and the Trustless Log Index	0	6.14	15-09-2026
3	EIP-8411: what segmented payload diffusion is made of	0	8.61	17-09-2026
4	Mempool Account Transaction Capacity from Historical Activity (MATCHA)	0	9.38	22-09-2026
5	EIP Editing Office Hour (EIP + ERC ) Meeting #108, July 28, 2026	0	18.32	27-07-2026
6	All Core Devs - Consensus (ACDC) #183, July 23 2026	0	15.18	13-07-2026
7	Same instruction count, 23x the wall clock: working-set effects in a deterministic RISC-V interpreter	0	10.98	18-09-2026
8	EIP Editing Office Hour (EIP + ERC ) Meeting #107, July 21, 2026	0	17.62	15-07-2026
9	EIP Editing Office Hour (EIP + ERC ) Meeting #111, Aug 18, 2026	0	18.71	13-08-2026
10	Evidence Review Framework for Project Applications in Decentralized Guilds/Agent Systems	0	8	19-09-2026

Классификация: . Схожих патентов: 0. Схожих новостей: 10. Тональность: 0. Информативность: 4.8. Источник: ethresear.ch.