發生什麼：形式化模型首次和 Core 的實際行為對照
btc-verified 是開發者 ProofOfKeags 以定理證明語言 Lean 4 撰寫的比特幣協議模型，GitHub 專案說明為「以 Lean 4 驗證的比特幣協議元件」，採 Apache-2.0 授權，2026 年 5 月建立。作者 2026-10-19 同步在個人網站與 Delving Bitcoin 論壇發表十月進度，題為「Connecting Map to Territory」，意思是要確認這張形式化的「地圖」真的對應現實中的比特幣網路。
作者指出，實務上定義比特幣協議的是 Bitcoin Core，但 Core 以現代 C++ 撰寫，直接做形式化驗證「以目前資源遠遠做不到」。因此他改走另一條路：讓 btc-verified 實作 libbitcoinkernel 的公開介面，再用差分模糊測試比對兩者行為。libbitcoinkernel 是 Core 把共識驗證程式碼切出成獨立函式庫的長期計畫。作者特別說明，這麼做不是鼓勵大家改用 btc-verified 的共識，而是借用 Core 團隊已畫好的邊界，作為衡量模型是否忠實的基準。
原始證據：九個函式、五類行為、一次 CI 執行
依貼文與專案 Fuzz/README，目前 btc-verified 以 Lean 實作了核心介面中的 9 個函式，涵蓋交易建立、複製、序列化、檢查及相關驗證狀態物件。測試工具直接建在 libFuzzer 上，把同一串交易位元組同時交給 Core 與 btc-verified，再比較可觀察結果。比對項目分五類：能否解析成交易物件（這和交易是否有效是兩回事）、序列化狀態與輸出位元組是否完全相同、不查 UTXO 也不執行腳本的交易本地檢查結論、回報的驗證模式與結果類別，以及先檢查一筆已知無效交易後，再檢查下一筆時狀態是否一致地被取代。
作者表示，在 10 月 18 日的 CI 執行中，這五類行為兩邊一致：共 100,000 次模糊測試執行、11 筆固定回歸輸入，結束時保留 264 筆語料。他也自行說明這些數字的意義：10 萬次是測試量，不等於 10 萬筆不同交易，突變輸入彼此相關；回歸輸入包括真實的傳統與 SegWit 交易、格式錯誤的編碼，以及剝除見證後恰為 999,999、1,000,000、1,000,001 位元組的三筆交易，因為隨機突變有 4,096 位元組上限，碰不到這個邊界。GitHub API 顯示該 CI 執行（編號 39158271308）於 2026-10-18 19:19 UTC 建立，結論為 success。
README 還提到一個負向對照：每次執行都會故意注入一個分歧，要求測試必須因為該結論改變而失敗、保存完整輸入與雙方觀察，且只在開啟注入時可重現。作者稱差分測試已列為合併前的 CI 檢查，觀察到與 Core 不一致就會擋下程式碼變更。這種跨實作差分測試的做法在比特幣生態已有先例，bitcoinfuzz 專案即以此方式在多個實作中找出錯誤。
限制：還不是共識驗證，也不是證明
目前範圍很窄。比對只涵蓋交易物件層級，沒有涉及 UTXO 集、腳本執行、區塊驗證或鏈狀態，作者也承認 btc-verified 「連最簡單地實作完整核心介面都還沒做到」。README 另註明，回報的拒絕類別不同時，只算介面層級的不一致，不會自動視為共識分歧。
作者自己也點出方法上的極限：抽樣測試無法建立普遍規律，下一個樣本隨時可能出現差異，這正是形式化驗證存在的理由。差分測試能做的，是在輸入越來越充分覆蓋程式控制流程時，降低兩邊行為分歧的機率。本文未獨立重跑該測試，數字皆為作者在貼文與 CI 紀錄中的自述。
AI 觀點分析與推論
AI 觀點：價值在於讓證明「有對象」
我傾向認為，這次進度的意義不在 10 萬次這個數字，而在方向：過去用 Lean 證明比特幣性質，常被質疑「證明的是你自己的模型，不是 Core」。若模型能經由 libbitcoinkernel 這條官方邊界持續和 Core 比對，未來在模型裡證出的定理，才有機會被合理地轉述成關於 Core 行為的陳述。對軟分叉審查來說，這類工具最有用的地方是替爭議規則提供可重現的檢驗，而不是取代審查者。
但我不會高估現階段成果。交易本地檢查是共識中最容易對齊的部分，真正會出現分歧的難點在腳本直譯、簽名雜湊、UTXO 與區塊層規則。若接下來幾個月 btc-verified 能把腳本驗證也接到同一套差分測試，而且仍維持零分歧，我會把它視為實質里程碑；若擴大範圍後頻繁出現介面差異，或因為 libbitcoinkernel 介面變動而必須不斷重寫，那這條「地圖對照現實」的路就會比作者預期更長。作者說下一個月的計畫是補齊其餘核心介面，這是最值得觀察的訊號。
