Leo Lara @ Thailand 🇹🇭 (leolara)

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.

• 1 reply
• 1 recast
• 1 reaction

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.

• 1 reply
• 0 recasts
• 1 reaction

Me too

• 0 replies
• 0 recasts
• 0 reactions

recast:farcaster://casts/0x7cb51682177a00244d45d6074390d67e97f66cf582a171339c181fd782ec8da5

• 0 replies
• 0 recasts
• 0 reactions