Anthropic 於十月二十二日經官方研究頁宣布，與 Theorem 合作，以 Claude 在 RISC‑V 組譯層面對一百二十三個真實開源庫完成大規模形式化驗證：把 Google OSS‑Fuzz 模糊測試入口轉成「在既定假設下對任何小於六十四 MB 輸入皆不崩潰」的規格，再以約一億八千萬行 Rocq 證明約二百三十九個入口點；官方自稱屬首次以人工智能大規模對生產軟件做組譯級形式化驗證，過程中 Claude 亦發現多年漏網的缺陷。來源真實性已對照 Anthropic 原文核實。

Anthropic／官方：以 Claude 大規模形式化驗證一百二十三個開源庫——RISC‑V 組譯級；約一億八千萬行 Rocq；與 Theorem 合作

Anthropic Frontier Red Team 於二〇二六年十月二十二日在官方研究頁《LLMs are making formal software verification feasible at a much larger scale》公布成果：與 Theorem 合作，以 Claude 在 RISC‑V 組譯指令層面對真實開源軟件產出可機器檢查的形式化證明。來源真實性已驗證。以下整理可核對的數字與方法、局限假設，以及對香港／亞洲企業軟件與資安落地的含義。

一、核心事件：把「模糊測試永不崩潰」寫成可檢查證明

官方可核對的主張包括：

規模：在 一百二十三 個不同 OSS‑Fuzz 開源庫上，對 二百三十九 個入口點完成「無崩潰」證明；
層級：證明作用於編譯後的 RISC‑V 可執行檔（組譯／機器碼），而非僅原始碼註解；
證明體量：合計約 一億八千萬行 Rocq；典型單份證明約 六十萬行，對應二進制中位數約 一萬八千 條 RISC‑V 指令；
規格來源：把開發者既有的模糊測試（fuzz test）自動轉成規格——「對任何小於 六十四 MB 的輸入，測試皆通過／不崩潰」；OSS‑Fuzz 對 C／C++ 常附帶 AddressSanitizer，記憶體錯誤亦會觸發崩潰；
合作與釋出：與 Theorem 合作；官方稱將公開部分證明、RISC‑V 與作業系統語意等可信元件；Theorem 亦表示可為其他開源項目跑同一管線，並發布 Claude skill 協助開發者起步；
定位：官方寫「就我們所知，這是首次以人工智能大規模把形式化驗證應用到生產軟件的組譯碼層級」。

證明過程中，Claude 亦被允許修補它發現的缺陷後再重新生成規格並繼續證明。官方舉例包括：僅在約二十 MB、特定版面輸入才觸發的解壓器計數下溢與越界寫入；需約六十四 MB 輸入與逾二 GB 記憶體的圖像解碼越界讀取；以及在 libexpat 重新發現 CVE‑2026‑56132（需深度嵌套輸入）等。文章強調：即便最終證明未完成，嘗試證明本身已能找出模糊測試不易觸及的缺陷。

二、技術原理：規格、模型與證明檢查器

形式化驗證要求先定義「正確」是什麼。官方指出多數應用難以寫出完整行為規格，因此採務實路徑：把已可編譯的測試套件（此處為模糊測試入口）編碼成規格，再配上 Theorem 的 RISC‑V 指令與 Linux 行程語意，機械地得到證明必須滿足的陳述；Claude 撰寫證明，Rocq 證明核負責檢查證明是否滿足規格。

在此管線下，開發者真正需要信任的主要是：（1）RISC‑V 與 Linux 行程的形式模型；（2）被證明的定理陳述本身；（3）Rocq 證明檢查器。證明正文極長，但幾乎不必人工逐行審閱——這是相對傳統「耗時數人年寫證明」的關鍵差異。官方亦提醒：形式化驗證不代表代碼絕對無缺陷；若規格或機器語意與現實不符，漏洞仍可能存在。

本次證明的明確假設包括：程式以單執行緒、靜態連結二進制、固定記憶體預算，在 RISC‑V CPU 上跑 Linux；輸入小於六十四 MB。多數實際部署若為 x86／ARM、動態連結 glibc，則不在目前證明範圍內——擴展需更多架構與作業系統語意。官方另述其他探索：以 Claude 為 RFC 1950（zlib）寫形式規格並在 x86 二進制上證明 Linux 核心實作符合規格；以 Verus 證明 Rust 寫的 Python 子集直譯器對照學術文獻中的 CPython 語意，並以逾一百七十萬個隨機 Python 程式實證行為一致率約百分之九十九點九五等。

效率方面，官方以三十六個小型驗證任務比較：Opus 5.5 在約少四成 token 預算下可證明其中一半，優於 Opus 5；代理之間共享已完成證明時，token 用量約再減百分之十七，顯示證明可複用。

四、日常應用場景

1. 開發者與平台工程

維護 C／C++ 關鍵庫、已接入 OSS‑Fuzz 的團隊，可把「證明管線」視為模糊測試的補強：先以現有入口生成規格，再評估是否引入 Rocq／技能／外部服務跑證明。實務上仍須處理修補審批、迴歸與發佈節奏；證明成功也不取代程式碼審查與供應鏈監控。

2. 企業與受規管行業

金融、醫療、關鍵基建若採購或託管大量開源依賴，可把「組譯級無崩潰證明覆蓋了哪些入口／假設」寫進供應商問卷與風險登記。香港持牌機構談操作韌性與第三方風險時，這類可機器檢查的產物比口號式「AI 已掃描」更易審計——但仍必須讀清楚假設邊界（架構、執行緒模型、輸入大小）。

3. 一般技術主管

可把故事讀成方法論轉變：當模型更擅於找洞與串連漏洞，防禦不能只靠更多測試；把測試升級成可檢查規格，是降低「未知未知」的一條路徑。現階段成本仍高（官方指證明可耗數億 token），宜先鎖定最高風險依賴。

4. 香港與亞洲市場視角

本地銀行、電商、政府相關系統大量依賴開源元件與雲端映像。Anthropic 這次示範的是「以前沿模型把形式化驗證拉近日常工程」的方向，而非即日可一鍵套用到所有 x86 微服務。對香港團隊，短期價值在於：（1）評估關鍵開源依賴是否已有／可申請類似證明產物；（2）把模糊測試入口與規格化思維寫進安全開發生命週期；（3）若要私有模型或資料不出境做安全代理／驗證工作流，需另案設計託管與權限。若貴機構需要在港規劃雲端資安、依賴治理或企業私有人工智能防護，可對接專業工程與顧問能力。

五、專業評價與潛在考量

優勢

官方研究頁提供可核對硬數字（庫數、入口數、Rocq 行數、輸入上限、假設清單），而非純願景稿。
證明檢查器與「可信計算基」邊界寫得清楚，有助專業讀者評估可轉移性。
與 OSS‑Fuzz 對接，對已有模糊測試資產的組織遷移成本較低。
附帶發現真實缺陷（含具 CVE 編號之例），顯示「嘗試證明」本身已有安全收益。
公開部分產物與 Claude skill 路線，降低跟進門檻。

需要留意的地方

「首次大規模組譯級」屬官方自稱，獨立學術對照仍待社群複驗。
目前假設（單執行緒、靜態 RISC‑V、Linux、小於六十四 MB）與多數雲端 x86／ARM 動態連結部署有落差。
AddressSanitizer 與選定入口並不覆蓋所有記憶體安全或邏輯缺陷；證明範圍外仍可能有洞。
證明成本高；企業導入需算清楚 token／人力與優先級。
Claude 可自動打補丁存在「為了可證而改程式」的獎勵駭客風險；官方稱已用懲罰與稽核緩解，買家仍應要求補丁審計。
本文不構成安全認證、合規意見或對任何開源庫的保證。

結語

Anthropic 與 Theorem 展示：以 Claude 把 OSS‑Fuzz 入口升級成 RISC‑V 組譯級「無崩潰」證明，並在一百二十三個庫、二百三十九個入口點累積約一億八千萬行 Rocq。對香港企業而言，重點不是今日就能為整套生產系統蓋章，而是形式化驗證正從「航電級稀缺工藝」走向「可規模化的工程選項」——前提是讀懂假設、檢查器與規格邊界。若貴機構需要在香港強化雲端與應用資安、開源依賴治理，或把人工智能納入安全驗證工作流，可參考 YSK Limited 的雲端遷移與網絡安全服務：https://ysk.hk/services/cloud-security

參考來源

Anthropic 官方研究：LLMs are making formal software verification feasible at a much larger scale（2026-10-22）— https://www.anthropic.com/research/formal-verification