Claude 而家唔止寫 code，仲會自己「自證清白」。Anthropic 同合作夥伴 Theorem 用 Claude 對現有軟體做數學驗證，幾週內生出大約 1.8 億行形式化證明碼（formal proof code），覆蓋 Google OSS-Fuzz 安全測試項目入面嘅 123 個開源庫。
點解呢件事有得睇？證明程式喺所有情況下無錯運行，歷來貴到嚇人——當年一個小團隊要 20 人年（person-years）先搞定嘅 seL4 作業系統核心，就係呢個方法嘅典型例子，所以形式化驗證（formal verification，用數學方法證明程式行為符合規格）一直只係航太艙位 software 呢類極端場合先玩得起。
重點唔係「寫新 code」，係「驗舊 code」。Claude 將崩潰測試轉成數學問題、分析編譯後嘅機器碼（machine code）、然後寫出成堆證明。有獨立驗證程式 Rocq 自動查證呢啲證明，Anthropic 話基本上唔使人審。研究員稱呢個係「全自主」證明生成——不過背後嘅工具同形式化基礎，係 Theorem 嘅人建嘅。
過程入面 Claude 揾到成百個 bug，而且被允許自己修。呢啲 bug 多數喺特定條件先會出頭，例如異常大嘅輸入檔或者特定存取序列，傳統測試根本攔唔到。有個廣用嘅 PDF reader，團隊一週揾到嘅安全 bug 數，等同該軟件一整年 typically 被報告嘅總數。另一個案例，Claude 捉到一個存在超過十年冇人發現嘅邏輯錯誤。Anthropic 強調，就算最後證明寫唔完整，嘗試本身都會帶出真實 bug。
但要注意邊界：「形式化驗證」不等於「無錯」。證明只喺嚴格條件下成立——特定處理器架構、單執行緒程式、輸入唔超過 64 MB。而現實中呢啲庫跑喺唔同硬件、唔同設定之上。算力開支都重，個別證明要幾億 token，Anthropic 冇披露整個項目總成本。另外一次小型測試顯示，Opus 5.5 用大約少 40% token 搞掂 Opus 5 一半嘅證明量。
阿調搞兩下：呢個唔係「AI 寫 code 好叻」嘅事，係「AI 寫 code 後點樣有人敢信」嘅事。形式化驗證一直係航空航太先有錢玩嘅奢侈品，而家被 Claude 壓到幾週嘅算力帳單。問題唔係 AI 夠唔夠聰明，係呢個流程有冇真正替代人審，定係人仲要坐喺後面睇住。Anthropic 話「幾乎唔使人」，但「幾乎」呢兩個字，先係真問題所在。
