Claude 寫數學證明，
證明程式唔會死機
以前要證明一段程式「點都唔會死機」，專家要花好多年。今次 Claude 幾星期內做咗 123 個程式庫。
TL;DR 先睇結論
Anthropic 將現有嘅隨機測試，改寫成一條數學命題。再叫 Claude 寫出證明。證明由獨立檢查器 Rocq 逐行驗算，呃唔到人。
結果係 239 個測試入口、123 個開源程式庫，被證明喺任何 64 MB 以下嘅輸入都唔會死機。寫證明途中，Claude 仲捉到幾隻潛伏多年、隨機測試一直撞唔到嘅蟲。
但記住最重要一句：「形式化驗證」唔等於「冇蟲」。證明只覆蓋一個好窄嘅範圍，下文會講清楚。
⏱ 60 秒圖解摘要（撳開）▼
一句講晒：由「試極都試唔晒」，變成「用數學一次過證明晒」——但只限證明寫明嗰個範圍。
舊方法：不停亂試，撞到算好彩
業界一直靠一種測試方法，叫 fuzzing。可以譯做「隨機亂入測試」。
做法好直接。程式開一個入口。測試引擎不停製造隨機資料，塞入去。
邊一份資料令程式死機，嗰份就係證據。證明程式有一隻蟲。
呢個方法好有用。Google 嘅 OSS-Fuzz 計劃就係咁捉蟲，行咗好多年。
但佢有一個死穴。輸入嘅可能性係無限嘅。你試一萬次、一億次，都只係試咗其中一小撮。
所以邏輯係咁：撞到死機，證明有蟲。撞唔到，只係證明你未撞到。
自己試下：點解亂試會漏咗隻蟲？
下面條軌係「輸入大細」由 0 到 64 MB。有一隻蟲，要大約 20 MB 嘅罕見輸入先觸發到。而一般 fuzzing 工具，餵嘅輸入通常細過 1 MB。
撳下面粒掣，開始亂試。
試幾多次都好，隨機輸入集中喺左邊細輸入區。20 MB 嗰隻蟲，永遠冇人掂過。呢隻蟲唔係假設——係今次研究真係搵到嘅，下文會講。
新方法：將測試變成數學題
Anthropic 冇掉棄舊測試。佢哋將舊測試「翻譯」成一條數學命題。
原本嘅 fuzz 測試問：「隨機試，會唔會死機？」新命題問嘅係另一回事：
「對於任何一個細過 64 MB 嘅輸入，呢個程式都唔會死機。」
「任何一個」係關鍵。證明咗呢句，意思係所有輸入一次過搞掂。唔使再逐個試。
成個流程係咁：
程式庫本身已有嘅測試入口，唔使重新發明「咩叫啱」。
程式編譯成 RISC-V 指令，再寫成一條要證明嘅命題。
Claude 針對機器指令逐行推理，寫出成份證明。
獨立檢查器 Rocq 改卷。證明啱唔啱，唔係 Claude 自己講，要過到檢查器。
點解以前冇人咁做？因為證明大得驚人。證明通常比原程式大好多倍，又要極專門嘅人手。
經典例子係 seL4 作業系統核心。人手寫個核心用咗 2 人年。驗證佢，用咗 20 人年。
而家唔同咗。寫證明呢種「量大、目標清晰」嘅苦工，正正係 AI 最擅長嗰種工。
成果：幾星期，123 個程式庫
成個過程只係幾星期。Claude 先修補途中搵到嘅蟲，再完成證明。
1.8 億行證明，冇人會逐行睇。亦唔需要。因為 Rocq 檢查器會驗算每一行。
人要睇嘅，只係最後嗰部分——「到底要信啲乜」。呢點去到第 5 節會講。
寫證明途中，順手捉到陳年蟲
證明寫唔通，通常即係程式真係有蟲。Claude 就自己修補埋，再繼續證明。
有幾隻蟲特別值得講。佢哋有個共通點：fuzzing 行咗幾年、試過以兆計次，都冇撞到。
解壓縮計數器出錯
一個解壓縮程式入面，有個計數器會「減過龍」。結果係寫入越界記憶體。
但觸發條件極刁鑽：要大約 20 MB 輸入，仲要係一種罕見排版。隨機測試餵嘅通常細過 1 MB，所以永遠撞唔到。
libexpat 嘅 CVE-2026-56132
XML 解析庫 libexpat 有一隻已編號嘅漏洞。觸發佢要輸入巢狀得好深。
Claude 喺證明過程中重新發現咗佢。呢類「要好深、好特定結構」嘅輸入，正係隨機亂試最弱嘅地方。
Linux 核心 zlib 符合 RFC 1950
Claude 先將 RFC 1950 技術文件寫成正式規格。再證明 Linux 核心入面嘅 zlib 實作，真正跟足份規格。
呢次證明唔止「唔死機」，而係「行為正確」。
Rust 版 Python 直譯器
Claude 用 Rust 寫咗一個 Python 直譯器，再證明佢跟 CPython 嘅語義。
實測跑咗超過 170 萬個隨機 Python 程式。有 99.95% 行為同 CPython 完全一致。剩低嘅係已知嘅邊角情況。
換句話講，就算最後證明唔成，「嘗試證明」本身已經係一部強力捉蟲機。
最重要嘅提醒：證明唔等於冇蟲
呢一點係 Anthropic 自己寫明嘅。唔係外界挑剔。
⚠️ 「形式化驗證」≠「冇蟲」
證明只保證一件事：喺證明寫明嘅條件底下，程式唔會死機。條件以外，證明咩都冇講。
而今次嘅條件，同你日常用嘅環境，有一段距離：
單線程運行。靜態連結（用 musl libc）。RISC-V 處理器。固定記憶體上限。Linux 進程模型。
大多數人用 x86 或 ARM 處理器。動態連結 glibc。多線程好常見。環境複雜得多。
仲有兩點要留意。第一，唔係每個測試入口都證明咗，證明唔到嘅只係公開咗命題，未有結論。第二，就算入口全部證明晒，都唔等於成個程式庫每個角落都覆蓋到。
咁到底要信啲乜？Anthropic 話，成件事最終只需要信任四樣嘢：
- RISC-V 模型對處理器行為嘅數學描述，要同真晶片一致
- Linux 進程模型對系統行為嘅數學描述，要同真系統一致
- 命題本身證明嗰句說話，要真係你關心嗰句
- Rocq 檢查器改卷嗰個工具，自己唔可以出錯
好處係：要檢查嘅範圍，由「成個程式庫每一行」縮到呢四樣。而且無論證明幾多個程式，呢四樣都唔會變大。
業界點睇
反應普遍正面。大家留意到一個轉變：
變成「檢查只係運算」。 寫證明要天才加年月；驗算證明，只需要電腦時間。
即係話，最難嗰部分——寫——而家有 AI 代勞。剩低嘅驗算，係機器嘅事。
但幾乎每個討論都會補返同一句：範圍限制要睇清楚。RISC-V、單線程、靜態連結，呢啲字眼唔係細節，係證明嘅邊界。
Anthropic 自己嘅講法都一致：呢個係起點，唔係終點。方向係將模型擴展到更多架構、更接近真實部署嘅系統。
一句記住
Claude 唔再靠「撞彩」捉蟲，而係寫出數學證明，等檢查器驗算——但證明保邊度，就只保邊度。
資料來源
- Anthropic 官方研究文章：LLMs are making formal software verification feasible at a much larger scale（2026 年 10 月 22 日）
- 合作夥伴 Theorem：theorem.dev（提供 RISC-V 與 Linux 進程嘅形式語義模型）
- RFC 1950（zlib 格式規格）：rfc-editor.org/rfc/rfc1950
本頁為 ELI5 解說，數字與說法以 Anthropic 官方文章為準。Anthropic 每週研究速報 · 2026-10-26。