Jolt字節碼67項中60項完成驗證，仍有7項待確認

LayerZero Research據報已完成Jolt zkVM 67項RISC-V字節碼擴充中的60項驗證，剩餘7項指令因涉及特定邊界案例，仍在驗證範圍內。

CryptoBriefing報導，LayerZero Research利用Lean定理證明器，歷時約兩個半月進行上述驗證。不過，相關數字與驗證論文尚未在LayerZero官方頻道獲得相同內容的確認。

形式驗證不是透過測試，而是以數學證明確認軟體是否符合既定規格。在zkVM中，若錯誤解讀指令或執行過程出現問題，錯誤結果可能被視為有效證明，因此這項工作相當重要。

Jolt的字節碼擴充會解碼ELF檔案中的原始RISC-V指令，並將其轉換為包含運算元、位址、電路旗標與查找旗標等資訊的內部表示。Jolt官方文件將字節碼描述為執行目標程式的基準。

擴充後的字節碼索引與ELF記憶體位址扮演不同角色。字節碼索引用於在執行週期中存取指令，ELF記憶體位址則用於確認程式計數器約束。

在執行過程中，系統也會證明讀取到的指令是否與預先處理的字節碼一致。因此，字節碼擴充階段的準確性，可能影響後續執行追蹤與證明結果的可信度。

這次驗證不代表Jolt整體已完成形式驗證。安德森·霍羅維茲（Andreessen Horowitz）在2024年的技術文章中表示，Jolt的驗證工作是逐步確認查找語義、多項式互動式證明、約束系統、RISC-V規格與實際Rust實作之間一致性的過程。

安德森·霍羅維茲的驗證路線圖也將確認形式化模型是否與實際實作程式碼一致列為獨立工作。換言之，即使Lean已證明形式模型，仍需進一步確認該模型是否準確反映實際實作。

既有研究曾運用ACL2定理證明器，驗證Jolt對RISC-V RV32I指令的查找語義。研究人員確認將指令拆分為小型查找表的過程是否符合RISC-V規格，並發現部分指令可透過最佳化減少不必要的查找。

相關研究指出，研究團隊已使用ACL2對完整RV32I指令集進行形式化與驗證。這次基於Lean的工作則採用不同定理證明器，確認Jolt字節碼擴充範圍，可視為既有驗證研究之外的案例。

LayerZero在Zero技術文件中表示，Jolt將作為網路的執行證明基礎設施。Zero的執行邏輯會經過證明生成與驗證程序，Jolt則扮演zkVM角色，證明程式執行結果是否正確。

不過，僅憑字節碼擴充驗證，不能據此認定Zero網路整體或Jolt整體的安全性已完成驗證。實際Rust實作與形式模型是否一致，以及其他證明組件的驗證範圍，仍需另行確認。

LayerZero與安德森·霍羅維茲公開的Akita與Lattice Jolt技術發表，則是探討零知識證明基礎設施密碼學組件的案例。這次工作聚焦於執行過程中的指令解讀與字節碼轉換，與先前以多項式承諾方式為重點的發表有所不同。

目前尚未公開已驗證的60項指令與未驗證的7項指令具體清單。尤其是7項指令涉及哪些邊界案例，以及實際實作程式碼與形式模型的一致程度，仍有待更多資料說明。

這次發表可定位為Jolt zkVM特定組件的形式驗證進展。由於驗證範圍有限，不能進一步解讀為整體zkVM或Zero網路已完成安全性驗證。