形式化驗證

ChainCatcher 消息，据 CryptoBriefing 報導，以太坊基金會研究員 Justin Drake 於 11 月 3 日宣布，leanVM 已實現端到端形式化驗證。leanVM 是一種極簡 zkVM，用於高效聚合基於哈希的後量子簽名，將多簽名打包為緊湊證明。性能上，leanVM 每秒可處理超過 1000 次 leanXMSS 聚合；leanXMSS 是計劃在共識層替代 BLS 的基於哈希的簽名方案。在 Devcon 8 上，Drake 將以太坊全面過渡至後量子安全的目標時間調整至 2028 年 12 月，以便為過渡所需的網絡分叉留出空間。該計劃依賴 leanVM、leanXMSS 和 leanSpec 三個開源項目，以太坊基金會正開發開源實現並推進形式化驗證，同時通過 Poseidon Prize 等激勵鼓勵創新。報導指出，leanVM 的形式化驗證證明了代碼符合規範，但 2028 年 12 月仍是目標而非承諾。

ChainCatcher 消息，以太坊機構隱私技術機構 EthSystems 宣布對其隱私池（shielded pool）完成了形式化驗證，範圍從書面規範一直到 Sepolia 測試網上運行的位元碼。驗證按層使用不同工具：模型、电路和哈希用 Lean，合約用 Halmos 和 Kontrol，錢包用 Aeneas 和 Verus，驗證器和部署通過逐位元重建核對。雙花和價值守恆已由 Lean 定理機器驗證。驗證中共發現 6 個問題，其中 3 個出在驗證工具本身。團隊同時列出了仍然依賴的假設：哈希無碰撞、驗證器會拒絕偽造證明、合約行為與模型一致。

ChainCatcher 消息，OpenAI 日前宣布，其 AI 模型破解了計算機科學中沿用二十多年的猜想指數時間假設，英文簡稱 ETH，並非以太坊。該假設關注特別難算的問題到底有多難，並以布爾可滿足性問題 SAT 為例：給定一組邏輯條件，是否存在一種賦值使所有條件同時成立。問題規模變大時，已知最好辦法基本只能逐個嘗試可能答案，時間開銷隨規模呈指數增長。指數時間假設進一步斷言，這類問題本質上無法被大幅加速，不存在真正意義上的亞指數時間高效算法。該假設自 1999 年提出以來，一直是理論計算機科學的重要基石，大量論文基於它證明某些問題很難、某些算法已接近最優。若指數時間假設被推翻，意味著許多被認為幾乎不可能更快的問題，理論上或許存在更好解法。OpenAI 聲稱，其模型找到一個確定性算法，能在亞指數時間內精確統計 k-SAT 問題的解的數量，並用 Lean 進行了形式化驗證。若該結果最終經得起專家審查，將直接動搖指數時間假設。

ChainCatcher 消息，人工智能公司 Anthropic 旗下 Frontier Red Team 於 10 月 22 日發布研究，稱大語言模型已能在更大規模上自動撰寫形式化證明。團隊與 Theorem 合作，使用 Claude 在 RISC-V 匯編層對超過 100 個真實開源庫證明安全性質，並稱這是已知首次用 AI 在匯編層對生產軟體做大規模形式化驗證。寫證明過程中還發現了多年未被發現的漏洞。實驗將 Google OSS-Fuzz 中已有的可編譯 fuzz 測試轉為規格：在單線程靜態二進制、固定記憶體預算、RISC-V CPU 與 Linux 等假設下，對小於 64 MB 的任意輸入，程式應正常退出且不觸發記憶體安全錯誤或斷言失敗。數周內，Claude 在修補所發現問題後，對 123 個 OSS-Fuzz 庫中的 239 個入口點證明了上述性質。證明針對編譯後的 RISC-V 指令，約 1.8 億行 Rocq，並由 Rocq 內核檢查。頁面稱，這並不等於這些庫沒有漏洞，剩餘問題可能位於受信任組件或證明範圍之外。頁面還稱，團隊讓 Claude 形式化 RFC 1950，並在 x86 二進制層證明 Linux 內核中的 zlib 實現符合該規格；用 Rust 編寫覆蓋 Python 大子集的解釋器，對超過 170 萬個隨機生成程式與 CPython 行為一致的比例為 99.95%。在 36 個小型驗證任務上，Opus 5.5 證明其中一半所需 token 比 Opus 5 少約 40%。團隊同時指出，證明針對單線程、靜態鏈接的 RISC-V 二進制，且證明檢查器不能判斷規格是否符合現實。

ChainCatcher 消息，据孫宇晨獎官方消息，該獎首批獲獎人已於 9 月 19 日正式進入 14 天公示。目前公示題目為題庫第 305、371、381、526、866、1001 號，其中 305、371、381 號問題的候選人為形式化驗證者，866、1001 號候選人為數學解題者，526 號則兩種角色皆有。公示信息已在官方 GitHub 候選登記表公開，公眾可提出正式挑戰。據悉，孫宇晨獎為全球首個基於題目清單的零信任去中心化學術懸賞機制，最高單題獎金 100 萬美元。設立當日已公布首批 66 個數學問題，最高獎 100 萬美元授予 OpenAI 研究團隊，以表彰其針對"三維納維--斯托克斯方程的存在性與光滑性問題"給出的解決成果及形式化證明。同時，獎項運營方還公布了獎池鏈上地址，已存入 1000 萬美元。公示期結束後獎金將以 USDT（TRC20）或 USDC（ERC20）進行發放，獲獎人也將獲得證書和獎牌。

ChainCatcher 消息，以太坊基金會形式化驗證團隊與 Yukon、zkSecurity 合作打造的開放自動研究挑戰 better.codes 現已上線。該平台將 Proximity Prize 中的自包含問題形式化於 Lean，並把 koalaIRS12 的機器檢查可靠性界放入公共排行榜，供任何人推動提升，以推進基於哈希的 SNARK 及後量子以太坊相關安全基準。求解者可自帶 AI 智能體，針對這一 Reed-Solomon 鄰近問題證明更高的可靠性下界，向固定的 128 位目標邁進。Lean 內核核驗每份提交，獲晉升的證明會提高公開界，其新引理、證明技術與不可能性結果將上游同步，供所有參與者復用。生產環境中多數哈希 SNARK 依賴相關鄰近間隙與相關約定結論，而目前可證明結果仍低於研究者所信基準，該挑戰旨在以開放、增量、可驗證方式縮小這一差距。koalaIRS12 源自相關論文並端到端形式化於 ArkLib。參與者可通過 GitHub 登錄並克隆挑戰倉庫，在固定定理陳述與驗證框架下提交；比較器與 Lean 內核確認後結果記入公共倉庫並注明求解者與所用模型。今日上線的是將 koalaIRS12 已證下界提升至 128 位的可靠性挑戰，後續或增加更多題目，細則以項目條款為準。

ChainCatcher 消息，Zcash 開發團隊宣布計劃透過即將推出的新隱私池 Ironwood 引入形式化驗證，以數學證明方式消除「無法檢測的增發漏洞」風險。此前消息，Orchard 屏蔽池存在的漏洞雖已完成修復且暫無證據顯示遭利用，但由於理論上無法透過鏈上歷史確認是否曾發生隱蔽增發，因此社區決定推出全新的 Ironwood 屏蔽池，並對其協議進行全面形式化驗證。

ChainCatcher 消息，ZEC 財庫公司 Cypherpunk 在 X 平台發文回應 ZEC 代幣市場波動，其表示，所有軟體都存在漏洞，歷史上比特幣曾因錯誤"多鑄"過 1,840 億枚 BTC。但這並不意味著應放棄區塊鏈技術，而是應透過形式化驗證與可證明正確性來增強安全性。Cypherpunk 強調，隨著 AI 技術的發展，漏洞檢測將更快、更廣，但關鍵在於誰能在惡意行為者之前發現問題，Zcash 透過即將發布的更新展示其具備這一能力。此前消息，隱私幣 ZEC 因被曝存在可能導致無限增發的安全漏洞而遭遇市場拋售，幣價一度單日跌超 50%。

ChainCatcher 消息，Vitalik Buterin 發文探討形式化驗證（Formal Verification）在區塊鏈安全領域的應用前景。文章指出，以太坊前沿研發中正興起一種新範式，直接使用 EVM 位元碼、匯編或 Lean 編寫程式碼，並用 Lean 中可自動檢查的數學證明驗證其正確性，研究者 Yoichi Hirai 將這一範式稱為"軟體開發的最終形態"。Vitalik 認為，AI 輔助形式化驗證有望同時提升程式碼效率與安全性，尤其適用於 STARK、ZK-EVM、抗量子簽名和共識演算法等安全核心模組。文章同時強調，形式化驗證並非萬能，仍可能因證明範圍不完整、規格錯誤、硬體側信道等問題失效；未來軟體或將分化為"安全核心"與"非安全邊緣"，以太坊將成為重要安全核心之一。

ChainCatcher 消息，Aptos 在 X 平台發文表示，Aptos 是首個支持動態調度形式化驗證的 L1，可數學證明其按設計運行。Aptos 稱，AI 編寫規範，數學證明其正確性，Move Prover 即為預言機，這是市場與機器的信任層。

ChainCatcher 消息，据 CertiK 官方消息，CertiK 已經完成對螞蟻集團創新開放式跨平台可信執行環境（TEE）HyperEnclave 的先進形式化驗證。據悉，螞蟻集團的可信原生技術團隊開發了開放跨平台軟體可信執行環境 HyperEnclave，旨在提高螞蟻集團隱私保護計算工作負載的效率和相容性。