軟體說它正確，
不等於直接相信

定理證明可以替程式寫下「它不會做什麼」的證據；零知識證明則想把那份證據壓縮、驗證，卻不必公開所有商業機密。

來源：Zero Knowledge Podcast Episode 406 ｜原始發表日期：2026 年 7 月 15 日

SCROLL

PART 1 ｜軟體正確，不是宣告而是命題

「沒有出錯」要先說清楚：
它究竟答應了什麼？

Alex Ozdemir 在這集訪談中把形式驗證說得很直接：要證明一個程式正確，不是看它跑過幾次，而是先寫下一個能涵蓋所有輸入的命題，再找出那個命題的證明。這讓問題從「這次有沒有壞」變成「它是否永遠不會違反指定條件」。

但這也留下重要邊界：定理可以被正確證明，卻仍然是錯的問題。受訪者提醒，安全戲劇往往不是證明器說謊，而是設計者寫了一個避開關鍵風險、或依賴不當公理的規格。形式驗證提高的是「命題到實作」的可靠性，不能替人決定命題是否完整。

可驗證的重點：不是程式貼上「已驗證」標籤，而是外部人能看到它聲稱保證什麼、用哪些前提保證，並檢查證據是否成立。

PART 2 ｜ ZK DSL、ZKVM 與抽象成本

訪談回顧 ZK 語言工具的演化：Circuit DSL 讓人直接描述證明電路；ZKVM 則把底層電路藏在虛擬機後面，讓應用開發者能以較熟悉的程式模型工作。這降低門檻，卻不是免費午餐：通用 VM 需要證明一套通用指令集的執行，對於追求極致效率的工作負載可能多了一層成本。

應用程式開發者描述想做的工作

抽象層ZKVM 或專門 DSL 決定怎麼表達

證明系統把執行或關係變成可驗證聲明

驗證者檢查聲明，不必重跑全部計算

Ozdemir 的立場不是二選一：ZKVM 很適合大量情境；但 VM 本身仍建在電路上，而某些高效能系統也仍需要針對特定問題設計證明關係。真正的設計題目是：誰要為便利、性能與可審查性付成本。

PART 3 ｜把 Lean 證明變成 ZK 證明

節目核心是 zkPi：它嘗試把 Lean theorem 和其 proof 轉成一份很小的零知識證明。驗證者可確認「這個公開命題確實有一份有效的 Lean 證明」，但不必取得完整 proof 的細節。這同時帶來隱私與簡潔性：大型證明可被壓成更容易傳遞與驗證的輸出。

不過，隱藏 proof 不代表隱藏 theorem。受訪者強調，命題、假設與公理必須仍是可檢查的；否則一個形式上正確、實質上避開問題的規格，仍能被當成安全保證販售。

形式驗證描述所有輸入下程式應遵守的性質。

零知識可隱藏證明細節，保留能驗的結論。

規格審查決定被證明的命題是否真正對應使用者在意的風險。

PART 4 ｜可信軟體的真正交接

這條路對專有軟體尤其有吸引力。公司不一定願意公開程式碼，使用者卻仍需要知道資料不會被濫用、特定安全條件是否成立。ZK 形式驗證提供一種可能：將完整實作留在內部，對外提供與公開規格相連的可驗證聲明。

但這不是免信任魔法。你仍要問：誰定義規格？規格覆蓋哪些系統邊界？資料輸入是否可信？更新後證明是否仍有效？本集的價值不在於宣稱問題已解決，而是把「軟體可不可以被信任」拆成能被逐段討論的工程問題。

真正值得驗證的，
不是「它有一份證明」，
而是「那份證明到底承諾了什麼」。

零知識可以縮小揭露範圍；規格審查決定這份保證有沒有碰到真正的風險。

Zero Knowledge Podcast Episode 406 保留 Alex Ozdemir 對 CirC、ZKVM、SMT、Lean、zkPi 與形式驗證邊界的完整技術脈絡。