Alex Ozdemir on where Theorem Provers and ZK meet

這場播客對話深入探討了形式驗證、定理證明與零知識証明在現代密碼學中的交匯點。

自 2021 年以來，ZK 領域的語言與工具生態發生了重大轉變。一方面，DSL 繼續演進，引入了隨機電路這一關鍵創新——電路不再是純粹的確定性計算，而是能夠採樣隨機挑戰、實現互動式證明系統的動態結構。Clean 等新 DSL 採用「驗證優先」設計，將驗證工具與語言協同設計。另一方面，ZK VM 的興起改變了開發者體驗——應用開發者無需理解電路細節，只需面對虛擬機介面，彷彿在用標準語言（如 Rust）編程。然而，這並非電路的終結。VM 實現本身基於電路，且 RISC-V 等通用指令集為零知識優化而非設計，導致性能開銷。因此生態正進入分層時代：對性能要求不高的應用用 VM，對性能敏感的應用（如 Google 的匿名憑證系統）仍需定製電路。

Cersei 編譯器基礎設施在這個演進中扮演樞紐角色。與傳統編譯器不同，Cersei 不是一對一的源-目標轉譯，而是一套可共享的編譯邏輯。它支持多個源語言編譯到多個目標：ZK SNARKs、多方計算、SMT 邏輯公式、整數線性規劃乃至全同態加密。過去兩年，Cersei 取得的核心突破是自動化隨機電路優化——不僅支持隨機性的使用，更能自動偵測確定性操作並替換為最優的隨機版本（如選擇四種記憶體論證中最合適的），甚至能合併冗餘挑戰、重組互動結構。這種動態優化對互動式証明的編譯是前所未有的。

與此同時，形式驗證成為確保編譯器正確性的關鍵。講者採用「驗證前」方法，聚焦有限域編碼這一易出錯的編譯階段，並發現了預期外的 bug——這驗證了預先驗證的必要性。為此，講者與團隊建構了 CVC5 SMT 求解器對有限域的支持，填補了此前的空白。現在，Z3、Yices 等多個求解器都支持有限域推理，形成了互操作的生態。

定理證明工具的選擇與應用同樣關鍵。SMT 求解器（自動定理證明）與 Lean（交互式定理證明）各有所長。SMT 專注於自動化，但僅限於預先定義的有限數學領域；Lean 允許人類定義複雜的數學結構（如同調），但需人工証明。兩者都已開始引入機器學習來指導證明搜索，但本質不變——SMT 承諾 100% 正確（找到證明），Lean 的內核極小且可驗證。這兩種工具甚至可協作：Lean 戰術生成 SMT 公式，SMT 求解後的證明被重新編碼為 Lean 可接受的形式。

講者新近的工作 ZK πι 代表了這些技術的融合。它解決了一個實際問題：專有軟體廠商如何向用戶證明「我的系統不會洩露你的資料」而無需公開原始碼？傳統方案要求開放源碼進行形式驗證；ZK πι 的方案是零知識證明一個 Lean 定理——定理敘述（如「系統不向第三方伺服器發送使用者資料」）保持可見供審查，但完整的 Lean 證明被隱藏。這需要 Mirage Plus 這樣的新證明系統，能高效地將依賴型檢查編碼為互動式電路。ZK πι 生成的証明僅 200 字節，相比數 MB 的完整 Lean 證明實現了顯著的簡潔性。

然而，形式驗證也面臨「安全劇場」風險。即便證明過程無懈可擊，虛假或不完整的定理同樣能被「證明」——例如，定理只指定四台伺服器的行為卻對第五台隱瞞。解決方案不是加密定理本身（ZK πι 正是因此而可見定理），而是警惕规范的完整性。這提醒我們：形式驗證解放了開發者對代碼的檢查負擔，但將責任轉移到對定理正確性的思考——這同樣不容懈怠。

#