以 Lean 驗證以太坊共識規格，找出序列化長度上限錯誤

值得記下的 5 件事

1. [0:20]
   通過測試之外，還要證明模型符合規格 講者表示，團隊從 Python 規格建立可執行的 Lean 模型，並以官方測試資料核對

   但目標不只通過既有案例，還要證明各種輸入下的行為一致；完整符合規格仍是持續進行的工作。

2. [4:20]
   高層共識證明仍有前提待補 講者描述，證明工作從單一區塊、單一節點的結果延伸至最終確定性，也就是區塊不再被撤回的性質

   不過，部分先決條件仍保留為假設，需要繼續證明，不能將已完成的部分解讀為整套共識已獲完整驗證。

3. [8:40]
   SSZ 證明檢查資料還原、編碼唯一性與長度 SSZ 是共識物件使用的序列化格式

   講者將證明擴展至更多規格型別，檢查編碼後再解碼能否還原原值、相同編碼是否對應相同值，以及編碼長度是否符合上限，而非只測幾個範例。

4. [10:00]
   長度上限漏算偏移表，驗證揭露公式錯誤 處理可變長度元素時，團隊發現舊上限只計入資料內容，沒有納入記錄資料位置的偏移表

   示例中的有效編碼因此超過原先上限；講者指出，問題出在上限公式，而不是證明嘗試本身。

5. [14:00]
   編碼唯一性不保證解碼器拒絕多餘內容 即使相同編碼只能對應相同值，也不能保證解碼器會拒絕多餘的輸入

   講者描述介面接受並忽略額外位元組的情況，這不違反既有的唯一性定理；尾端多餘位元組的問題仍未解決，規範解碼的證明也是後續工作。