Rust 的安全承諾，仍需要驗證邊界
Rust 以所有權、借用檢查與型別系統排除大量記憶體錯誤，但這不等於所有 Rust 程式都已被證明安全。官方《Rustonomicon》明確區分 Safe Rust 與 Unsafe Rust：後者讓開發者執行型別系統無法保證安全的低階操作，常見於硬體、作業系統、外部函式介面與效能敏感程式。即使完全不用 unsafe，越界存取、整數溢位或對 None 執行 unwrap()，仍可能造成 panic。參考：https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html
2026 年 7 月公開的 HarnessLLM 論文，瞄準的正是形式化驗證落地時一項不顯眼、卻昂貴的工作：撰寫 verification harness。這類 harness 不只是測試案例，而是告訴模型檢查器「如何呼叫目標程式、哪些輸入可自由變動、必須檢查什麼性質」的驗證入口。原始論文與完整數據見：https://arxiv.org/abs/2607.22161
HarnessLLM 實際怎麼運作
來源事實：HarnessLLM 並未要求 LLM 從空白開始猜測 API 用法，而是把既有測試套件當成「開發者已寫好的使用情境」。其流程可拆成四個階段：
- 掃描 Rust 的中介表示 MIR，找出含有 unsafe、
unwrap或編譯器插入 assertion 的候選函式，並定位相關測試。 - 從測試中的 assertion 與前置敘述抽出個別呼叫情境，再把常數提升為函式參數；系統會重播情境並比對執行軌跡，確認轉換後仍保留原本行為。
- 針對自訂型別建立建構子相依圖，逐層找出可公開呼叫的建構方法，再讓 LLM 產生 Kani 所需的非決定性輸入。
- 交由 Kani 編譯；若失敗，將錯誤訊息回饋給 LLM，最多修正十輪。系統同時鎖定不得任意改寫的程式區域，並以語法樹比對原始專案，攔截 LLM 虛構的型別或函式。
這套設計的關鍵不在於「LLM 很會寫 Rust」，而在於把 LLM 放進受約束的工具迴路：測試案例提供語意線索、相依圖縮小問題、編譯器淘汰語法與型別錯誤、Kani 負責真正的模型檢查。換句話說，LLM 是 harness 合成器，不是安全性的裁判。
數字亮眼，但代表什麼要看清楚
來源事實：研究團隊在九個 crates.io Rust 函式庫、494 個測試案例上抽出 294 個呼叫情境；以執行軌跡是否與原測試一致衡量，情境保留精確率為 94.66%。系統最終為 294 個情境全部產生可編譯 harness，使用 GPT-4.1 時每個平均耗時 145 秒。相同情境交給 Kani 的 Autoharness，成功率為 41%。論文的消融實驗也顯示，拿掉型別相依圖形成的建構指引後，首次產生正確 harness 的比例平均下降 23.1%。完整方法與實驗細節見：https://arxiv.org/html/2607.22161
研究另在 pdf-rs 0.9.0 找到六個問題，包括整數溢位、陣列越界與非字元邊界操作，論文標示其中五個已修正。案例之一把原本固定十個位元組的測試輸入改成長度及內容皆可變的符號向量，Kani 因而探索到長度不足兩個位元組時的越界路徑。這比「程式成功編譯」更有說服力，因為它展示了 harness 確實能把單點測試擴成一組受限但廣泛的狀態空間。
合理推論：真正的生產力提升，可能不是省下幾分鐘打字，而是讓團隊能把原本只會抽查少數高風險函式的形式化驗證，擴展到更多 API 情境。尤其自訂 struct、enum 與彼此相依的建構參數，正是單純自動產生任意值容易卡住之處。
容易被「100% 成功率」掩蓋的限制
首先，100% 指的是 294 個既有情境都產生了語法與型別正確的 harness，不代表所有程式行為都被涵蓋，也不代表已得到無條件安全證明。Kani 官方說明，模型檢查可能證明性質、提出反例，也可能耗盡資源；其 Rust 功能支援亦非完整，例如目前不支援所有並行程式情境。參考：https://model-checking.github.io/kani/getting-started.html
其次，HarnessLLM 的情境來源仍是既有測試。論文自己的稀疏測試實驗顯示，harness 生成成功率可以維持，情境涵蓋率卻會下降：工具能忠實放大已知用法，卻不保證發現測試作者從未想到的 API 組合。94.66% 的情境保留率也意味著轉換並非零誤差，剩餘案例仍需人工檢查。
第三，bounded model checking 必須設定陣列長度、迴圈展開與遞迴深度等界線。界線太小可能漏掉錯誤，太大則可能讓求解器耗盡時間或記憶體。論文承認目前部分界線由 LLM 依程式內容推定，尚未自動解決這個核心問題；此外，表層 Rust 程式碼的追蹤可能漏掉巨集生成的函式。
作者觀點：因此，HarnessLLM 最合理的定位不是「形式化驗證自動化完成」，而是降低進入模型檢查前的工程門檻。它把專家的工作從逐一手寫 harness，轉向審核情境、限制條件與反例是否合理；專業判斷沒有消失，只是移到更有價值的位置。
對台灣系統軟體與韌體團隊的意義
台灣常見的韌體、驅動程式、網通設備與嵌入式軟體，都涉及硬體介面、FFI、二進位格式解析或高效能資料處理，也是不得不接近 unsafe 邊界的場景。若團隊正把部分 C／C++ 元件改寫成 Rust，HarnessLLM 類流程的價值在於：既有測試不再只是回歸檢查，也可成為建立符號輸入與驗證情境的原料。
但導入順序應從高風險、界線清楚的函式開始，例如協定解析、長度計算、緩衝區操作與 FFI 包裝層，而不是直接以整個產品的「驗證成功率」作為 KPI。對供應鏈與資安稽核而言，可重現的 harness、明確的展開界線、Kani 版本及反例紀錄，會比「使用了 AI 驗證」更有實際意義。
後續值得追蹤的指標
- 是否在更多、更大型且含並行或巨集密集程式的 Rust 專案重現結果。
- 新增情境覆蓋率、分支覆蓋率與誤轉換率，而不只報告 harness 可編譯率。
- 六個問題的修補與上游確認紀錄，以及其他研究團隊能否獨立重現反例。
- 界線選擇能否由靜態分析輔助，並清楚區分「有界證明」與資源不足。
- 不同模型、Kani 與 rustc 版本下的穩定性、成本，以及生成程式碼的人工審核量。
HarnessLLM 值得注意之處，不是讓 LLM 取代形式化方法，而是用編譯器、程式分析與模型檢查器約束生成模型，把既有測試轉成更廣的驗證入口。它距離「按一下就證明整個 Rust 專案安全」仍很遠，卻可能讓形式化驗證第一次成為一般系統軟體團隊可以逐步導入的工程流程。