發生什麼：兩條規則被證明「合起來夠用」
BIP-54（共識清理，Consensus Cleanup）是 Antoine Poinsot 與 Matt Corallo 提出的軟分叉規格，一次處理時間扭曲攻擊、極端慢速區塊、64 位元組交易造成的 Merkle 樹弱點，以及重複 coinbase 交易。其中針對時間戳有兩條新規則：每個難度週期的第一個區塊，時間戳不得早於前一個區塊 7200 秒以上；每個週期的最後一個區塊，時間戳不得早於同週期第一個區塊。
Pieter Wuille 9 月 17 日在 Delving Bitcoin 發文，問的是這兩條規則是否足夠，還是仍有未知攻擊能讓鏈無限加長。他的結論是足夠：在時間上限 t、累積工作量上限 w 之下，鏈長 n 有封閉式上限，長期出塊速度最多約每 9 分 56 秒一塊，另外只能多出一段需付出難度上升代價的有限區塊。10 月 21 日（UTC）他更新首帖，把「給定鏈長與時間、反推最少工作量」的較精確公式併入，並把十進位近似式也納入 Lean 證明。
原始證據：數字與證明的範圍
Wuille 以 2026-09-09 21:30 UTC 的狀態示範：當時距創世區塊 557,982,895 秒、真實鏈高 966,270（含創世共 966,271 塊）、累積工作量約 2 的 96.35 次方。代入公式的上限是 1,012,794 塊，較精確的工作量公式反推為 1,009,930 塊；他目前找到的最長可行鏈為 1,007,326 塊。上限比真實鏈多約 4.8%。若只保留其中一條規則，上限仍超過 33.4 億塊，相差約 3300 倍，這是「兩條缺一不可」的依據。
證明檔用 Lean 4 與 Mathlib 寫成，模型照搬 Bitcoin 的難度調整：時間跨度夾在 1/4 到 4 倍、目標值截斷成 nBits 緊湊格式，以及整數除法。README 要求編譯後只依賴三個標準公理，不得出現 sorry。Wuille 在首帖寫明：證明由 LLM 產生，他沒有審閱證明本身，讀者只需檢查被證明的命題是否正確。我們下載並核對了證明檔內的三個定理名稱與 README，但沒有自行重跑編譯。
為什麼要算這個：區塊頭防 DoS
Wuille 在討論中說明動機：Bitcoin Core 2022 年合併的 headers presync（PR #25717）會先在不存檔的情況下預先同步對方的區塊頭，確認累積工作量達到門檻後才重新下載並存下，以免被大量低難度的假區塊頭塞滿硬碟。現行邏輯只能依中位數時間規則假設鏈長最多每秒 6 塊；若 BIP-54 啟用並固化，攻擊鏈的長度上限會降到略高於真實鏈，防護參數可以收得更緊。
狀態要說清楚：BIP-54 規格標示為 Complete，但 Bitcoin Core 的實作 PR #35793 標題就寫明「不含主網啟用」，至今仍未合併；規格也沒有啟用方式與日期。Wuille 的推論以「已啟用並固化」為前提，現在的節點不受影響。
AI 觀點分析與推論
AI 觀點：這份證明降低的是「修得夠不夠」的爭議，不是「要不要啟用」
我傾向認為，這份工作最大的價值在於把時間扭曲修補從「看起來夠」變成「有上限可算」。過去討論常卡在是否還有交替時間戳一類的變形攻擊；現在若要主張還有漏洞，就得指出 Lean 命題本身與共識規則哪裡不符，門檻高很多。討論串裡 Zawy 一度質疑可能出現無限區塊，後來也自承誤解，說明這個框架能把爭論收斂到可檢查的命題。
但它不會直接推動啟用。BIP-54 其餘三項修補（慢速區塊、64 位元組交易、重複 coinbase）不在這份證明範圍，啟用方式也還沒有共識。受益最直接的是節點實作者與輕節點的區塊頭驗證；一般持幣人短期沒有要做的事。另一個限制是證明由 LLM 產生且作者未審：若日後有人審閱命題時發現建模與實際共識規則有落差，結論就要打折。我會觀察兩個訊號：PR #35793 是否進入合併或附上啟用參數，以及是否有第二位開發者公開審閱 Lean 命題。
