zkWasm完成電路形式驗證，但部分邏輯未納入

CertiK於2024年完成的zkWasm核心電路形式驗證成果近日再次受到關注，但這並非2026年新完成的工作，而是對既有研究結果的重新介紹。

CertiK在2024年技術部落格中表示，已驗證zkWasm的Halo2電路在滿足有效約束條件時，是否代表符合WebAssembly（Wasm）執行規則的狀態。開發商Delphinus Lab也於2024年5月2日宣布，其自行實作的zkWasm已完成形式驗證。

zkWasm是一套在執行Wasm程式後產生零知識證明的系統，讓驗證者無須重新執行完整計算過程，也能確認結果是否有效。程式執行追蹤會轉換為Halo2的多個表格，驗證者則確認各表格是否滿足既定的算術約束。

形式驗證不同於一般程式碼審計。它不只尋找已知漏洞模式，也會將「程式在特定條件下是否依照既定規則運作」轉化為可由機器確認的數學命題。

在zkVM中，單一電路可處理多種程式執行。因此，確認電路約束是否符合Wasm實際執行語意，是判斷證明健全性的核心步驟。

CertiK公開儲存庫說明，以Coq撰寫的形式驗證涵蓋zkWasm電路的主要組成，包括執行表格、記憶體表格、呼叫堆疊與位元運算。目標是證明，在所有電路約束均獲滿足時，執行追蹤中的每一列都代表符合Wasm執行規則的狀態。

公開內容也顯示，驗證過程在電路的記憶體存取以及呼叫與返回結構中發現問題，並完成修正。這說明形式驗證不只是檢查既有程式碼，也能找出規格與實作之間的不一致。

不過，這不能解讀為「整個zkWasm已完成全面驗證」。公開儲存庫包含Coq模型、證明程式碼與編譯流程，但以Rust撰寫的完整演算法並未納入驗證範圍。

公開程度也存在限制。即使儲存庫公開了驗證程式碼，部分電路組成、指令解碼邏輯、Wasmi直譯器與Halo2的運作方式仍被視為假設，或排除在驗證範圍之外。

Wasmi直譯器、Halo2本身以及部分約束產生程式碼同樣未納入驗證。外部呼叫功能與部分指令解碼邏輯，也依賴額外假設或人工審查。

CertiK表示，對應的內部儲存庫共有3萬3080行Coq程式碼。程式碼規模公開，與完整公開證明範圍是兩個不同問題。

CertiK的2024年年度報告指出，驗證對象是由144條指令組成的zkWasm電路，並將其評價為零知識證明生態中的首個完整形式驗證。這是CertiK自身的說法，獨立比較標準或同儕評審結果尚無法由公開資料確認。

CertiK表示，相關形式驗證框架可套用於其他zkVM與zkEVM。不過，這只是公司對適用可能性的說明，不代表其他系統已完成驗證。

Delphinus Lab分享其自行實作的zkWasm完成形式驗證，並連結CertiK的技術文件。開發商的正面回應已獲確認，但不代表驗證範圍已擴大至整個軟體堆疊。

CertiK其後介紹，使用Verus重新實作部分過去的zkWasm證明，並將程式碼規模從2440行縮減至595行。這項工作與最初宣布完成驗證的工作不同，不能視為原有驗證公開範圍的擴大。

相關研究已以〈Formal Verification of Circuit-Soundness in zkWasm, a General Purpose zkVM〉為題，列入ACM CCS 2026預定發表論文。論文研究團隊包括CertiK、Delphinus Lab、NVIDIA、哥倫比亞大學與耶魯大學研究人員，但論文全文與審查結果的詳細內容，僅靠公開資料尚無法確認。

這起案例顯示，zkVM基礎設施正嘗試以數學方式說明電路的正確性，並已形成具體研究成果。同時，也有必要區分公開驗證範圍與可重現性，不能將其直接延伸解讀為整套軟體的安全性。