SizzLean：形式化验证的 Lean4 SSZ 库，已补齐大部分验证缺口

SizzLean 是一个用 Lean 4 实现完整 SSZ 栈的独立项目（非 EF 发布），已对共识协议所用全部 SSZ 类型完成编解码三大核心性质（往返、非可延展性、大小上界）及 Merkle 化相关的机器校验证明，并通过上游一致性测试语料。