We had SizzLean running already in May, but we present it here now because we have closed most formal verification gaps at this point.
SizzLean is a Lean 4 implementation of the full SSZ stack with machine-checked proofs of the three central properties of the codec, proved across every SSZ type the consensus protocol uses. The library passes the full upstream conformance corpus. It is an independent project, not an EF release. In pcaversaccio’s formal-verification thread I earlier reported SSZ proofs in progress; the status there is updated now, specifically about SSZ part of Etheorem project. Repo: etheorem/packages/SizzLean at main · etheorem/etheorem · GitHub (packages/SizzLean).
Proofs
SSZ has two halves, the byte codec, serialization and deserialization, and Merkleization, the hashing of a value into its tree root. The proofs cover both, stated once, generically over the whole SSZ type language, and proved for every type in the covered set.
The codec half rests on three theorems:
- Roundtrip: for any well-formed value, deserializing its serialization gives back the original value. This rules out a codec that loses or alters data.
- Non-malleability: distinct values never share an encoding. Two different states cannot serialize to the same bytes, which closes the doctoring route where an attacker substitutes a different object under a valid encoding.
- Size bound: an encoding never exceeds the size bound that the schema computes statically. Offsets, counts, and bounds can then be trusted without runtime re-derivation.
The Merkleization half carries proofs of its own, at the same level. The cached Merkle tree the library uses for speed is proved to agree with the spec’s Merkleization for every type in the covered set, from the per-shape root agreement up to a fresh box’s hashTreeRoot. The update path is proved beside it: single and batched writes keep the root correct. And the openings and generalized indexes the light-client and data-availability sides consume come from a proved model of the index computation. A client that computes roots and proofs through this library runs on proved code end to end.
The covered set for both halves excludes only zero-width shapes. Everything else in use by the consensus spec is included, and a script in the repo recomputes the covered-type count from the built library. Concretely, the set covers uintN for all six widths from 8 to 256 bits, bool, vector and list over both fixed-size and variable-size element types, bitvector, bitlist with its length marker in the final byte, and container over any field list, fixed-only or mixing fixed and variable fields.
The README’s coverage table records the proof technique type by type. The integer types route through a little-endian digit codec, proved by induction on the width. The bit types rest on a byte-packing inverse, proved injective per byte chunk. The variable-size shapes decode through a uint32 offset table, with proofs that reassemble the value from the written offsets and the sliced scopes.
Conformance runs beside the proofs, against the pinned upstream ethereum/consensus-spec-tests corpus. Both presets pass clean: ssz_generic 2188 / 2188 wire-format cases, ssz_static 1585 / 1585 on mainnet and 38991 / 38991 on minimal, every fork from Phase 0 through Fulu, including the ePBS containers. The 292 progressive-container cases sit outside the library’s type language, no adopted fork uses those types, so the harness classifies them as out of scope.
The library is also tested by using it in a Consensus specs implementation in Lean4. A sibling package in the same repository implements the consensus specs themselves in Lean 4, containers, state transition, fork upgrades, and fork choice at Fulu, Gloas and Heze built directly on SizzLean for all serialization and hashing, and checked against the per-fork consensus test vectors. The SSZ layer under it is thus tested the way a spec client would drive it, real containers at full state scale, not only wire-format fixtures. All consensus vector tests pass.
A proof ledger in the repo records, row by row, what each theorem does and does not establish.
The trust base is small and easy to check. Every reliance on the native SHA-256 enters the proofs through three named axioms, sha256Hash_eq_spec, sha256Combine_eq_spec, and sha256BatchCombine_eq_spec, each stating that the fast implementation equals the pure specification. Nothing else. #print axioms on any central theorem reports only the three standard kernel axioms every Lean theorem may use. One grep lists the whole inventory:
grep -rEn '^axiom |^@\[extern' packages/SizzLean --include='*.lean'
The proofs were developed with heavy AI assistance. Lean checks each proof against its kernel.
Using it in your project
One line declares a type:
structure Validator where
pubkey : Vector UInt8 48
withdrawalCredentials : Vector UInt8 32
effectiveBalance : UInt64
slashed : Bool
activationEligibilityEpoch : UInt64
activationEpoch : UInt64
exitEpoch : UInt64
withdrawableEpoch : UInt64
deriving SSZRepr
The deriving handler inspects the field types, builds the SSZ shape, and generates the instances. Serialization, deserialization, hash-tree-root, and the three central theorems for that type come out of it. You never write proofs by hand, and none are needed: the theorem instances are generated from the same shape the codec uses, so the guarantee and the implementation cannot drift apart.
A function over your types can stay abstract on two axes, the backend and the hash function. A box in SizzLean wraps a value together with its hash tree, and it carries both as parameters, the backend on the value side and the hash function H on the hashing side. A spec function is written once against that abstraction:
-- schematic; see MANUAL.md for the exact surface
def activate (box : SSZ.Box H T) (i : Nat) : SSZ.Box H T :=
sszUpdate box validators[i].activationEpoch := CURRENT_EPOCH
At the call site you instantiate the box with either backend, and with whichever hash function you need. The cached box runs the function for execution, rehashing only the path from the changed field to the root, and batching multi-field updates across overlapping paths. The pure box lets the same definition reduce under the Lean kernel, which is what a proof needs. A proof about activate is written against the pure instance, and it holds for the cached instance because both backends implement the same abstract interface. No duplicated source sits between the verification path and the runtime path, which is the drift this design removes.
The hash parameter swaps the same way. A future hash function, whatever the post-quantum work settles on, replaces SHA-256 without touching your containers, your spec functions, or your proofs; the cache machinery, the deriving handler, and the theorems are all generic in the hash, so the change is one instance at the call site.
A pure-Lean SHA-256
Everything above leans on one primitive, and the library ships its own implementation of it. LeanSha256, a sibling package, is a SHA-256 written entirely in Lean, with the compression function and the message schedule proved against the FIPS 180-4 specification. It passes the NIST CAVP test vectors, runnable with one command, and it reduces under the Lean kernel, which lets the SSZ proofs treat hashing as a computable function rather than an opaque oracle.
The pure implementation is the specification side of the trust story. For execution, the library calls a native SHA-256 over an FFI, and the three axioms above say exactly one thing, that the native result equals the pure result. Since the pure side is itself proved against the standard and checked against the CAVP vectors, the axioms carry little weight, and replacing the native implementation later, or proving the equivalence instead of assuming it, leaves every dependent theorem unchanged.
The team
SizzLean is built (as part of Etheorem project) 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 especially to irajgill, who wrote many of the SSZ proofs.
In the philosophy of Invisible garden one aspect of this project is learning, we are learning Formal Verification by doing but we were not experts previously. People are welcome to join us and co-learn. Any review, feedback, contribution and, of course, use is welcomed.
Questions for feedback: what would be more interesting for us to improve in SizzLean?