Bend-SSZ: Formally proving SSZ

1

Disclosure: this is an AI generated report. if you are not okay with it. don’t read it, I wont bother giving it a human touch. I think it is good enough.

SSZ is one of those things in Ethereum that everybody uses and nobody thinks about. Every consensus client has to serialize the same objects into the exact same bytes and compute the exact same Merkle roots, and if two clients disagree on a single byte, that is a consensus split. And yet, the way we make sure clients agree today is test vectors. Test vectors are great, but they only cover the inputs someone thought of writing down, and in my experience the nasty bugs are always in the inputs nobody wrote down (a weird offset table, a bitlist with a stray padding bit, a length that overflows a 32-bit counter).

So I tried something different: write an SSZ library where the implementation is proved to do what the specification says, for every single type, instead of being tested against a few thousand examples. In this post I will go over how the library works, what exactly is proved, how we tried to break it, and (most importantly) what you still have to trust.

What it is

The library is called bend-ssz. It covers all 109 mainnet Fulu types plus the 131 generic forms of the official test suite, so 240 types in total. It is written in Bend, a language whose type checker is also a proof checker, which means the code and the proofs about the code live in the same place and get checked by the same tool. Bend also compiles to C, so the thing you prove is the thing you run.

The library gives you, for every type: decode, encode, hash_tree_root, and a typed object API (getters and setters for fields, get/set/append for lists, and cached Merkle trees for incremental roots).

How it works

There are four layers, and only the first two need to be trusted as written:

  • The spec, transcribed. I took simple-serialize.md (consensus-specs v1.6.1) and wrote it down in Bend as plain, boring definitions: what a value is, how it serializes, how it deserializes, how it gets Merkleized. This part is frozen and hash-locked, and it was audited separately against the prose spec and a Python reference port.
  • The schemas. The 109 Fulu schemas and the generic forms, pinned (the same ones consensus-spec-tests use).
  • The implementation. Generators (Python) write a fast implementation for every type. It works on packed 32-bit words, not on the spec’s lists of bytes, so it is genuinely a different program from the spec (otherwise proving them equal would be cheating).
  • The proofs. The same generators write the proofs. The generators are not trusted: whatever they produce has to pass the checker, run from scratch before anything gets merged.

Under the hood

A few details for the people who will want them:

  • Representation. A decoded object is a typed, owning value: fixed-size parts are packed little-endian into U32 words (a Bytes32 is 8 words, a uint64 is 2), lists keep their length next to their word storage, and lists of variable-size elements hold each element in a box. Decode is two passes over the input window: a generated validator (offsets, lengths, padding bits, selectors) and then a generated reader that copies storage out of the input. Nothing points back into the input buffer.
  • Sizes. All size arithmetic is 32-bit and saturating: the largest accepted encoding is NMAX = 2^32 - 32 bytes, a size that does not fit becomes the marker 0xFFFFFFFF and stays poisoned through + and *, and every encoder refuses a poisoned size instead of writing a wrapped one.
  • Decode with a budget. X_decode_checked_budget(buf, size, budget) first computes X_dcost(size) = ((size >> 3) + 1) * K + 2^19 heap words (saturating) and refuses before reading anything if that is above budget; otherwise it is exactly X_decode_checked. K is per type: 40 for blocks and ExecutionPayload, 7 for BeaconState, at most 7 for everything else.

Some numbers

Runtime speed, Bend’s native C backend against Go fastssz (pinned, via go-eth2-client), one thread each, median ns/op on the official fixtures:

type (fixture size) operation bend-ssz fastssz ratio
BeaconState (2.74 MB) deserialize 0.68-0.74 ms 0.73-0.76 ms 0.9-1.0x
BeaconState (2.74 MB) serialize 0.75-0.82 ms 0.75-0.85 ms 1.0x
BeaconState (2.74 MB) hash_tree_root 74.5-82.8 ms 17.3-18.1 ms 4.2-4.6x
SignedBeaconBlock (17-24 KB) deserialize 14.9-28.0 us 24.1-34.9 us 0.6-1.0x
SignedBeaconBlock (17-24 KB) hash_tree_root 0.63-1.04 ms 0.13-0.20 ms 4.7-5.3x
DataColumnSidecar (6.5-19 KB) deserialize 1.7-4.3 us 3.3-8.2 us 0.5x
Attestation (237 B) deserialize 0.49-0.62 us 0.31-0.34 us 1.5-1.9x

Over all 978 measured workloads the median ratio is 0.8x for deserialize (worst 3.0x, on small types where fixed overhead dominates), 0.7x for serialize (worst 2.8x) and 3.9x for hash_tree_root (worst 7.6x). The hashing gap is mostly SHA-256 itself: Go uses the CPU’s SHA instructions, while bend-ssz uses a pure-Bend SHA-256 (on purpose, so the hash is the same code everywhere), and a single 64-byte compression is already about 4x slower. Big caveats: these were measured on an earlier toolchain (Bend 2.0.25) before the last round of hardening, on a loaded machine, and the fixtures are the spec-test states (a handful of validators), not mainnet sized. I will re-run them before anyone quotes them.

What is proved, in numbers

In one sentence: for every type, the bytes we write are the spec’s bytes, decode accepts exactly the canonical encodings and rejects everything else, and the root is the spec’s root. Plus laws for the object API (setters, list operations, cached roots).
Types covered 240 (109 Fulu mainnet + 131 generic test forms)
Public, hash-locked statements 5,827
Files the proof checker accepts 14,731
Full check from scratch 17.5 min on 20 cores (9,847 CPU seconds)
Official test vectors 295 ssz_static + 5,145 ssz_generic, all passing
Spec transcription audit 60 rules, 6,841 constants, 48,279 differential cases, 0 disagreements

Trying to break it

A proof only proves what its statement says, so the real question is: what did we forget to state? To find out, we did a lot of mutation testing (deliberately breaking the implementation and checking whether some proof notices):

What How much What happened
Automated mutation of the spec layer 1,049 mutants all killed except 4, which were proved equivalent
Hand-written, spec-driven faults, 10 rounds, a fresh auditor each round 2,000+ faults every survivor got a new law, was shown unreachable, or was documented. On the parts earlier rounds had already covered, the share that slipped through fell from ~25% to under 10% in the latest rounds; each round that went somewhere new found a fresh pocket (round 9: plain element access on most vector and list kinds had no laws at all, 140 critical survivors, all closed by one generator; round 10: 12 of 342 survived, all unpinned default constructors)
Crash hunts on the public API, 7 rounds 2M+ hostile decodes across all 240 types and real BeaconState / blocks, plus 1.6M random operations on the cached Merkle trees 0 crashes; findings went from 9 in round one to a single low-severity one in each of the last rounds

Every round found something, which honestly was the point. Two of the things we found are worth sharing because I think any SSZ library can get them wrong:

  • Size arithmetic. Lengths near 2^32 wrap around in 32-bit math. The library now supports encoded objects up to 2^32 - 32 bytes, with saturating size arithmetic that is proved to agree with the spec.
  • Decode memory amplification. A valid message can cost way more memory to decode than its size. A block whose payload has a million one-byte transactions is about 5 MiB on the wire and about 28x that once decoded. We measured all 240 types over 438 worst-case shapes:
type worst shape decoded heap per input byte
blocks, ExecutionPayload transactions full of 1-byte transactions 28.5-28.7
the same full of empty transactions 27.4-28.0
progressive test containers inner lists full of empty lists 22.0
everything else, BeaconState included at most 2.6

The reason is structural: every variable-size element is a box plus an array slot (24 bytes for the slot alone, 86 for an empty transaction), and its only cost on the wire is a 4-byte offset. On the network this is bounded (a block has at most 2^20 transactions and messages are capped at 10 MiB, so roughly 150 MiB of heap and about 0.24 s of decode in the worst case), but anything that decodes without a size cap is exposed. So the library has the budgeted decode above, which refuses those inputs before allocating anything. (K is measured, not proved: every one of the 438 shapes decodes within at least 1.4x margin of its bound, and a dedicated crash hunt did not manage to beat it.)

Running it in an actual client

Proofs are nice, but I wanted to see it inside a real node. So we linked it into Prysm through a small C interface (decode only, Prysm still serializes and hashes in Go, behind a build tag). Against Prysm’s own decoder it agrees on the official ssz_static vectors, 105,150 mutated inputs and 66,300 random objects, with the only differences being inputs where Prysm’s decoder is more lenient than the spec.

Then we ran a Kurtosis devnet with three consensus clients: one Prysm checking every single decode against its own decoder, one Prysm decoding only through bend-ssz, and one Lighthouse. All three kept the same head and finalized, with 57,000+ decodes through bend-ssz and 0 mismatches. To be clear, this is a correctness thing, not a speed thing: through the C boundary (and the copy that turns a Bend object into a Go struct), decoding is 2-10x slower than Go’s native decoder, about 2.3x for a BeaconState and 2.9x for a signed block. The native numbers above are what the library does on its own; the FFI glue is where the time goes.

What you still have to trust

In my personal opinion this is the most important section, so I will be blunt:

  • The spec transcription. It is the reference. If it is wrong, we proved the wrong thing. It is small, frozen and differentially tested, but at the end of the day it is something a human has to read and agree with.
  • The checker. We use Bend’s checker with one change that is not merged upstream (it lives in my fork). Also, its logic has Type : Type, so there is no consistency proof for it. Our proofs only use Type in boring ways, but that is an argument, not a guarantee.
  • The compiler and the runtime. Bend’s compilation to C is not verified, so a compiler bug would only be caught by tests.
  • SHA-256 and a few premises. SHA-256 is a parameter, and some theorems have premises (listed in the repo).
  • Known gaps. Four of the generic test types have their decode proved only up to 2^29 or 2^31 bytes, the memory-budget factors are measured, and there are a few “unchecked” entry points whose contracts the caller has to respect.

A word on how this was built

Almost all of the code, the proofs and the audits were written by AI agents, and every change only got merged after a cold full check, regenerated generator outputs and re-verified frozen statements. That is also the biggest caveat: nobody independent has reviewed this yet. So if you want to help, the most valuable thing you can do is read the spec transcription and the list of public statements and tell me where they are wrong.

Overall, I think this shows that proving an SSZ implementation correct end-to-end is very doable today, and that the interesting part is not the proofs themselves but everything around them: what you state, what you forget to state, and what you trust.

Links:

Thanks for reading!

1 Like