Verus 為 Rust 補上形式驗證，把正確性從測試變成證明
Amazon Science Blog · 2026-08-31
Verus 把 Rust 原本只能靠測試抽樣涵蓋的邊界情況，改成用求解器做數學證明：開發者直接在原始碼裡以 requires／ensures 寫下前置與後置條件，Verus 在驗證階段檢查程式碼在「所有可能輸入」下都成立，而不是測試案例挑到的那幾組數字。Amazon Scholar、卡內基美隆大學教授 Bryan Parno（Secure Foundations Lab 主持人）在 Amazon Science 部落格文章中說明，Amazon 已經用 Verus（verus-lang/verus）證明 Nitro Isolation Engine 的關鍵元件正確。
原本的問題
Rust 的型別系統能擋掉記憶體安全問題，但擋不住邏輯錯誤。文章舉例：C 語言陣列越界會有不可預期的後果，Rust 遇到同樣情況只是「安全地當機」，並不代表程式邏輯本身正確；Rust 也無法保證程式算出的結果符合預期，或不會外洩不該外洩的秘密。傳統測試只能檢查抽樣輸入，容易漏掉邊界情況——文章以 binary search 為例：target 剛好是陣列最後一個元素，或 target 根本不存在，都是測試容易略過但規格必須涵蓋的情形。
對 unsafe 程式碼與自訂鎖（custom locking）的並行程式，問題更明顯：一旦標成 unsafe，編譯器就不再檢查安全性，正確與否全靠人工審查；並行程式裡誰拿到鎖、拿到的值有沒有維持不變性，Rust 型別系統同樣管不到。
核心改動
Verus 讓開發者在既有 Rust 原始檔裡直接加規格與證明，正常的 Rust 編譯器會忽略這些標註，所以同一份程式碼可以同時被驗證過與未驗證的專案（包含用 Cargo 建置的專案）消費。以 Verus 官方範例 requires_ensures.rs 裡的函式為例：
// 一般 Rust：呼叫端傳入範圍外的值，release build 靜默溢位，
// debug build 才會 panic，且沒有任何保證回傳值等於預期結果
fn octuple(x1: i8) -> i8 {
let x2 = x1 + x1;
let x4 = x2 + x2;
x4 + x4
}// 加上 Verus 標註後：
fn octuple(x1: i8) -> (x8: i8)
requires
-16 <= x1 < 16,
ensures
x8 == 8 * x1,
{
let x2 = x1 + x1;
let x4 = x2 + x2;
x4 + x4
}requires 是前置條件：呼叫端必須保證 x1 落在 -16 到 16 之間，否則過不了驗證；ensures 是後置條件：回傳值 x8 必須精確等於 8 * x1，不只是「沒當機」。驗證在編譯期由求解器完成，文章指出開發者通常一秒內就能拿到回饋，快到可以在 VS Code 之類的編輯器裡即時看到驗證失敗的紅波浪線，形成互動式開發迴圈；同樣的自動化與速度也讓 AI agent 能更快疊代產生證明。文章也提到，Verus 可以驗證含數千行程式碼與證明的完整專案，速度接近早期驗證工具處理單一函式所需的時間。
對並行程式，Verus 允許替鎖加上不變性屬性：拿到鎖的人必須拿到滿足該屬性的值（例如「這個值永遠是偶數」），釋放鎖前必須重新證明值仍滿足屬性；Verus 也能證明鎖實作本身正確。文章特別點出，這對 Nitro Isolation Engine 這類依賴複雜自訂鎖換取效能的程式尤其重要。
影響範圍
Amazon 內部已經用 Verus 證明 Nitro Isolation Engine（負責替 Nitro hypervisor 執行虛擬機隔離）的關鍵元件正確，以及其他安全關鍵基礎設施，細節留待後續文章說明。Amazon 是 Rust Foundation 創始成員，Rust 也用在 Firecracker（支撐 AWS Lambda 與 AWS Fargate）等專案上，這類「跑在隔離邊界上、出錯代價極高」的程式碼是 Verus 目前鎖定的對象。
文章列出的開源案例，指出哪些場景已經在用 Verus 補齊測試覆蓋不到的正確性：
- Vest（secure-foundations/vest）：輸入二進位格式描述，自動產生附帶正確性與安全性證明的解析／序列化程式碼。
- Verdict（secure-foundations/verdict）：可證明正確、支援自訂驗證政策的 x.509 憑證驗證函式庫。
- CapybaraKV（microsoft/verified-storage）：驗證持久記憶體日誌的正確性與當機安全性，確保系統斷電或當機時資料仍維持良好格式。
- Anvil（anvil-verifier/anvil）：證明 Kubernetes controller 的正確性與 liveness，確保在合理假設下系統最終會收斂到穩定狀態。
- Atmosphere 微核心與 CortenMM 記憶體管理系統：分別是以 Rust 開發並用 Verus 驗證正確性的微核心，以及採用可擴充鎖定協定、其並行程式碼經 Verus 驗證的記憶體管理系統。
對正在用 Rust 寫儲存引擎、憑證驗證、並行資料結構、或 unsafe 程式碼這類「測試覆蓋不到邊界就會出事」路徑的工程師，這篇文章給出的具體做法是：先替最關鍵的少數函式加上 requires／ensures，用 Verus 的求解器把邊界情況變成可驗證的規格，而不是無限堆單元測試個案；由於回饋通常在一秒內，這個過程可以直接嵌進日常開發迴圈，不必等整套 CI 跑完才發現規格被破壞。
原始來源：Amazon Science：Developing provably correct Rust code with Verus、verus-lang/verus (GitHub)