事件背景：編譯通過不等於行為已被證明
2026 年 9 月提交的 Corten，是一套在 Rocq 證明助理中驗證 Rust 程式的研究框架，底層採用 Iris 分離邏輯。論文主張，其主要突破不是「又一個 Rust 除錯工具」，而是首次把接近原始碼的表層 Rust 語意連同程式邏輯機械化，並直接以 Rust Reference 為依據。原始論文：https://arxiv.org/abs/2609.04372
來源事實：Rust 的所有權、借用與型別系統能在編譯階段排除大量記憶體錯誤，但官方文件明確指出，unsafe 並未取消未定義行為；它只是把維持安全條件的責任交給程式設計者。更重要的是，Rust Reference 也警告，目前仍沒有一套完整形式模型界定所有 unsafe 行為。這代表「Rust 很安全」與「某段系統程式符合其規格」是兩個不同命題。官方說明：https://doc.rust-lang.org/stable/reference/behavior-considered-undefined.html
Corten 如何運作
Corten 的入口不是較低階的 MIR，而是 rustc 編譯流程中的 Typed High-level Intermediate Representation（THIR）。程式先經 hax 與 hax2rocq 轉入 Rocq；由於 THIR 仍保留較多原始 Rust 的運算式與控制流程結構，證明目標中的抽象語法樹可以重新顯示成接近原始碼的形式。相較之下，MIR 已拆成基本區塊與暫存值，驗證者往往還得反推它們對應到哪一行程式。
其核心語意採「最弱前置條件」：先指定執行後必須成立的條件，再計算執行前至少要擁有哪些條件。Iris 分離邏輯則用權限描述記憶體的所有權、共享與分割；Corten 將結構化值抽象成由欄位及元素組成的樹，藉此追蹤誰可以讀寫哪一部分。Iris 官方將自身定位為實作並驗證於 Rocq、可用來推理程式安全與資料抽象的高階並行分離邏輯框架：https://iris-project.org/
值得注意的是，Corten 對 safe 與 unsafe Rust 使用同一套所有權邏輯。安全程式通常由借用檢查器預先排除衝突；unsafe 程式則必須在證明中自行交代權限義務。論文甚至把借用檢查器放在可信基礎之外：證明規則不把「編譯器接受了借用關係」當成前提，而是直接要求所需的所有權證明。
架構上，Corten 刻意分成公理語意、程式邏輯與證明自動化三層，並以 interaction trees 的指稱語意逐項建立可靠性。語法導向的策略會依目前的 Rust 結構選擇規則、整理控制流程，再處理所有權分割與合併；去函數化的 continuation stack 則避免巢狀控制流程讓證明目標膨脹成難以閱讀的高階函數。
為何現在值得注意
合理推論：Corten 真正競爭的不是單次找錯速度，而是證明能否跟著原始碼長期維護，以及不同軟硬體元件能否在同一語意基礎上組合。既有 RefinedRust 已證明，Rust 的基礎式驗證並非空白領域；其 2024 年論文同樣使用 Iris 與 Coq，從 MIR 轉譯並驗證含 unsafe 指標操作的簡化版 Vec。因此，Corten 的新意應精確理解為 THIR／表層程式語意與證明可讀性，而不是「第一個驗證 Rust 的系統」。交叉查證：https://iris-project.org/pdfs/2024-pldi-refinedrust.pdf
實際成果，也揭露了成本
來源事實：在合成測試集中，自動化證明約比直接展開語意的證明短二至四倍；但規格本身平均約為 Rust 程式的兩倍長，自動化後的證明仍約為原程式的二至四倍。換言之，這是降低形式化工程成本，不是消除成本。
研究另驗證一個約 300 行、使用大量模式比對等慣用寫法的 buddy allocator。包含規格的 Rocq 證明約 2,800 行，其中約 1,400 行用於重新建立空閒區塊串列的不變量。證明涵蓋配置與釋放時維持記憶體表示及串列良構，並確保回傳區塊不與剩餘狀態重疊；它沒有證明最佳配置策略、碎片率上限，也依賴尚未證明的 Rust core 函式規格。
容易被「基礎式驗證」四字掩蓋的限制
- 語言覆蓋仍在擴充：trait 僅部分支援；Iris 雖能處理並行推理，Corten 尚未實際驗證並行 Rust。
- 目前抽象位元組記憶體模型是單執行緒；
transmute、無鎖原子操作及記憶體映射 I/O 等依賴實際位元布局的程式，不適合直接套用現有抽象。 - 複雜
Drop解構子的驗證仍屬後續工作，公理語意的可靠性也尚未涵蓋全部已支援語法。 - 可信運算基礎仍包括 Rocq 核心、rustc 的解析與型別檢查，以及尚未獨立驗證其 THIR 轉譯正確性的 hax／hax2rocq。
作者觀點：因此，Corten 現階段較像可擴充的研究地基，而非下載後即可替整個 Rust 專案背書的產品。最有價值的訊號，是論文坦白列出證明邊界、可信基礎與未完成項目；形式化驗證的可信度，往往正取決於這些範圍是否說得清楚。
對台灣讀者的意義與觀察指標
對從事晶片控制軟體、韌體、作業系統元件、工控或資安產品的台灣團隊，Corten 提供的不是「改用 Rust 就自動安全」，而是一條把 unsafe 邊界、配置器與硬體介面契約納入機器檢查的可能路徑。較務實的導入方式，是先鎖定小型但失效代價高、介面穩定的核心元件，而非企圖一次驗證完整產品。
後續應觀察四件事：所有已支援語法何時都有完整可靠性證明；unikernel 與 THIR-to-MIR 編譯器案例能否公開並由第三方重現；Rust core 與標準函式庫規格能否補齊；以及原始碼改版後，證明修改量是否真的低於 MIR 路線。若這些指標逐步成立，Corten 才可能從漂亮的語意架構，走向可負擔、可稽核的工程工具。