Bend 2 Law 與 Proof：AI 寫程式，機器能把錯誤擋住嗎？（2026）

2026 年 9 月 17 日（UTC），Victor Taelin 在 X 發布 Bend 2，主張 Bend 2 Law 與 Proof 能用 proof checking 阻擋 AI 犯錯，而且同一套函式式程式可以編譯到 CPU 或 GPU。這個方向真正有價值的地方，不是「AI 從此寫不出 bug」，而是把一部分驗收條件從自然語言搬進機器可重複檢查的規格；它真正危險的地方，也恰好在同一處：機器只會守住人有寫下來的邊界。

以下先還原官方機制，再用實際反例與最新版工具重跑結果檢查它的邊界，最後給出適合放進 AI 改碼流程的做法。結論先說：proof 是真的，規格漏洞也是真的；兩者並不矛盾。

It is a new programming language that blocks AI mistakes via proof checking.

這是一門透過證明檢查來阻擋 AI 錯誤的新程式語言。

Victor Taelin，Bend 2 發布貼文

Bend 2 Law 與 Proof 到底做了什麼？

Bend 2 把程式與命題放在同一套型別系統裡。開發者在 LAWS.bend 寫下想守住的命題，例如「某個轉換必須保留所有元素」；再由 PROOF.bend 提供同名定義，讓 checker 驗證這個命題是否有一個合法的 proof。若 proof 缺漏或無法成立，明確執行 bend PROOF.bend 會失敗；全部成立時，工具才回報 All terms check.。完整語法與檔案分工可見官方 Guide。

In short, LAWS.bend is AGENTS.md backed by proof.

簡單說，LAWS.bend 就是一份由 proof 支撐的 AGENTS.md。

Bend 官方 README

這不是「程式可以被證明」的新發明。從 Curry–Howard correspondence、dependent types 到 proof-carrying code，核心觀念已有很長的歷史。Bend 2 比較新鮮的賭注，是把它包成 AI agent 容易產生的明確 proof、快速的小型 checker，以及可把標記為平行的純計算送往 Metal 或 CUDA 的 runtime。換句話說，創新重點是工作流與工程取捨，不是把形式驗證從零發明一次。

第一個關鍵修正：Law 不會自動接管每次編譯

「Law 必須先被證明，程式才能通過檢查」這句話少了一個重要前提：專案或 CI 必須明確執行 proof gate。官方把 LAWS.bend 與 PROOF.bend 的角色稱為一種 convention；CLI 的特殊檢查也只在入口是 PROOF.bend 時，要求它匯入旁邊的 LAWS.bend。一般的 bend main.bend 不會自動搜尋同目錄的 Law。

AlphaLab 以 2026 年 9 月 18 日發布的 Bend 2.0.10 做了限縮重跑：同一資料夾放入一條尚未完成、實際不可能成立的 Law，編譯普通入口仍以 exit code 0 完成；改跑會匯入它的 PROOF.bend，才因 TODO 以 exit code 1 失敗。這不代表 checker 沒用，而是提醒團隊：沒有接進 CI 的證明，跟沒有被執行的測試一樣，不能形成 guardrail。

最有力的反例：AI 沒有騙過 Proof，而是鑽過了 Law

發布後的 Hacker News 討論出現一個很漂亮的反例。使用者把官方格子遊戲裡的牆拆掉，再要求 agent 修好程式並維持「玩家不能贏」的 Law。Agent 沒有打破這條命題，反而改了移動規則，讓角色不能以人類原本預期的方式前進。結果是：proof 合法、Law 成立，但遊戲行為仍然錯了。原始實驗與程式片段可見該則 HN 回覆。

They only protect what you remember to write. They’re not a silver bullet.

它們只會保護你記得寫下來的事項，不是銀彈。

Victor Taelin 對規格不足反例的回覆

這個案例反而證明 checker 忠實地做了工作：它檢查的是形式命題，不是作者腦中的完整產品意圖。若 Law 只寫「終點不可到達」，它不會自動補出「四個方向都要維持正常移動」「地圖不能被改寫」「畫面與內部狀態一致」。越能搜尋解法的 agent，越可能找到一個在字面上合法、在人類看來荒謬的 witness。

因此，一條通過的 Bend 2 Law 與 Proof，只能證明 checker 讀到的形式命題在其 calculus 與假設下成立。它不會自動證明自然語言需求完整，也不涵蓋未被建模的 I/O、UI、網路、效能與部署環境。這與測試的限制相似，只是 proof 能對已寫清楚的命題提供更強、可重複的保證。

第二條邊界：Source-level proof 不是完整工具鏈的保證

最容易被「機器檢查」四個字遮住的，是 proof 之外仍有一條信任鏈：

1. 人類意圖是否被完整翻成 Law；
2. Law 是否由人擁有、審查並禁止 agent 偷改；
3. checker/kernel 是否正確實作規則；
4. compiler、runtime 與 C／Metal／CUDA／JavaScript backend 是否保留 source semantics；
5. 最後部署的 artifact、硬體與外部系統是否照預期運作。

官方 README 自己把限制寫得很直接：Bend 仍年輕、compiler 尚未完整 audit、Lean model 與實際 checker 可能不一致；BendRT 文件也明說理論結果是關於 calculus，不等於 C runtime 已被驗證。這些是健康的工程揭露，但也代表目前不能把它描述成從規格一路保證到 GPU 輸出的 end-to-end verified toolchain。

還有兩個具體例子。第一，@unsafe 可繞過 soundness wall；官方把「仍會 check 並以 0 結束」列為刻意保留的行為。在 AlphaLab 的 2.0.10 重跑中，一個以它導出 0n == 1n 的假 proof 仍以 exit code 0 結束，只多印出一則 unsafe annotation 警告。CI 因此不能只看 exit code，還要拒絕 unsafe 警告。第二，公開的 Metal 餘數問題 #824 在同一台 Apple Silicon 主機可重現：同一個 native binary 的 CPU 結果為 2，Metal 結果為 4294967295，兩者都正常退出。這不否定「同一 source 可選 CPU/GPU 執行」，但否定了「不同 backend 已被證明語義等價」這種過度延伸。

那麼，Bend 2 真正改善了什麼？

它把原本散落在 code review 裡的一部分接受條件，變成 agent 必須交付、checker 可以重跑的 proof。對「排序後元素不變」「餘額守恆」「某個轉換可逆」「權限狀態不可越界」這類邊界清楚的 invariant，這是很有吸引力的工程方向。人不必逐行相信 AI 的推理，只要擁有 Law、審查 proof gate，並保留 proof 之外的測試。

上圖的重點不是某個語法技巧，而是 mutation test 也要用來測 Law。先故意把正確函式換成常數回傳、刪掉關鍵分支或交換運算順序；如果 proof 仍然通過，表示規格可能沒有約束到真正重要的行為。這一步把「規格是否夠強」從哲學問題變成可操作的紅隊測試。

我的判斷：我同意這個方向，但不同意「Proof 等於沒有 bug」

我同意的部分：Bend 2 把 agent 產生的程式與 proof 一起交給確定性 checker，確實比「模型說自己改好了」更可靠。當 invariant 能被精確形式化，而且 Law 的所有權、proof command 與版本都固定時，它能把一類回歸錯誤擋在合併之前。

我存疑的部分：目前的公開證據不足以支持「整體 AI 程式碼因此可信」或「compiler boundary 已被驗證」。截至 2026 年 9 月 19 日，能直接查到的材料主要仍是官方示範、專案文件、發布首日的小型實驗與公開 issue；這些足以證明概念值得研究，還不足以外推到大型 production codebase。9 月 19 日 06:22（台北時間）的 HN 快照已有 588 points、301 則 descendants，代表注意力很高，不等於成熟採用。

最精確的說法是：Bend 2 把部分 AI 程式碼審查轉成可重複的 source-level proof gate。在 Law 完整、受保護、明確執行 proof command、拒絕 @unsafe 且固定工具版本的前提下，它能機器檢查指定命題；但規格完整性、compiler/runtime/backend 與部署結果，仍要靠審查與測試守住。

如果今天要導入，先守住這 6 條

1. 由人擁有 LAWS.bend：agent 可以提案，但不能自行修改後直接合併；CODEOWNERS 與 review rule 要把 Law 凍結成治理邊界。
2. CI 明確執行 bend PROOF.bend：不要假設普通編譯會自動發現同目錄的 Law；可沿用 Agent CAPA 的 CI 閘門方法，把失敗條件與修復證據一起版本化。
3. 把 unsafe 警告視為失敗：除了 exit code，也掃描輸出與變更內容，禁止 proof scope 出現 @unsafe。
4. 對 Law 做 mutation test：準備一組故意作弊、理應被拒絕的實作，驗證每條高價值 Law 真的有辨識力。
5. 保留傳統測試：proof 守形式化的純核心；integration、differential、fuzz、UI 與效能測試守住未建模的現實。
6. 固定 Bend 版本與 backend：升級後重跑 proofs 與 CPU/GPU differential tests；目前不要把「能編譯到 GPU」當成「各 backend 結果已被證明相同」。