EthPadThai

Five Ethereum consensus clients must agree on every state transition, or the chain splits. So how complete are the tests for the functions that define those transitions? Today that question is answered by expert judgment, case by case. No systematic process stands behind it, so the gaps stay invisible. I wanted a number. The consensus specs are executable Python, so you can read each function as a model and list every input scenario it treats differently. Every assert is a partition boundary. Every branch is a dimension of variation. Map the existing tests onto that list and the gaps become visible. The technique is old. Category-partition testing dates to the 1980s. What is new is applying it to executable specs that are themselves the protocol. For process_proposer_slashing it was 25 scenarios, 18 covered, 72% scenario coverage. The gaps led to new tests, now merged, raising it to 96%. Documenting another function the same way surfaced a real spec bug: a helper inherited from an earlier fork that the new builder flag silently broke. A filled-in partition table also works as a precise spec for an AI coding agent. You hand it one exact scenario to implement. The judgment of what matters stays with you. The full method is in the post, with the partition tables and the worked examples. Thanks to @brechy and @danceratopz for the review. steel.ethereum.foundation/bl…

Most SSZ libraries are tested against the spec. I built one where the core properties are formally proved, in Lean 4. It also passes the full upstream test corpus. SSZ is how Ethereum serializes and Merkleizes its data — if hash_tree_root or deserialize is wrong, you get the kind of bug that can split the chain. For this reason I wanted something that is not only tested against the spec, but also proved. Formal verification. The library is called SizzLean. I proved three theorems: roundtrip (decode after encode returns the same value), non-malleability (two different values cannot produce the same encoding), and a size bound. They hold for the fixed-size SSZ types: the integers, bool, fixed vectors and lists, and containers built from those. I have not proved them yet for bitvector, bitlist, and variable-size containers. So this is a base, not a finished proof. Trust boundary. The only thing I assume without proof is the C SHA-256 function, declared as three named Lean axioms. You can list the full trust footprint with one grep, or with #print axioms on any theorem. Nothing else is taken on trust. Two backends. The same spec runs on a fast cached backend, used for execution and for running the test vectors, and on a pure backend, used for the proofs. I put the hash function behind a typeclass, so SHA-256 can be replaced by Poseidon2 or a post-quantum hash without changing the containers, the proofs, or the cache. Conformance. On top of the proofs, it runs the official ethereum/consensus-spec-tests on both presets: ssz_generic: 2188 / 2188 ssz_static (mainnet): 1585 / 1585 ssz_static (minimal): 38991 / 38991 This covers every fork from Phase 0 to Gloas, including the new ePBS containers. I also commented the code to be read. If you want to learn how SSZ works, or how to do this kind of work in Lean 4, you can follow it from top to bottom. The verification was done with heavy help from an AI coding agent. With Lean this does not change the result: the kernel checks the proof, independently of who wrote it. I work on specs and test vectors at the Ethereum Foundation, on the STEEL team. This is a personal project. The next step is to widen the proofs toward the remaining types. Repo and full details: github.com/etheorem/etheorem…

I am training hard to debate with some of the brightest minds at the Ethereum Protocol Day this Sunday organised by @0xpantarhei and @DappLearning . Looking forward to bleeding edge ideas cooking on Ethereum and of course the best food in the world!!