剛剛讀完Vitalik關於形式驗證的最新文章，真的值得一讀。他基本上在描述為什麼以太坊領域的開發者越來越傾向於這種方法：用低階語言撰寫程式碼，然後透過數學證明來驗證正確性，而不是僅僅依靠測試來捕捉所有問題。

這裡有趣的是人們對安全性思維的轉變。與其依賴經驗性測試和程式碼審查（傳統方法），逐漸出現一種新範式：開發者透過機器可驗證的證明來驗證程式屬性。這就像將安全性從「我們認為這是安全的」轉變為「這在這些方面絕對不可能失敗」。這個生態系已開始將此應用於關鍵基礎設施——EVM實作、STARK證明系統、抗量子簽名，以及像零知識證明這樣支撐現代加密通訊的協議。

但重點來了：Vitalik提醒這並非萬靈藥。形式驗證有其實際限制。安全定義仍取決於人類如何建模問題。有些系統過於複雜，無法完全形式化。而硬體層或未經驗證的模組也可能成為攻擊面。即使有堅不可摧的數學證明，如果你的規格錯誤或遺漏了假設，仍然存在漏洞。

Vitalik提出的更實用的看法是將形式驗證與其他方法結合——如AI輔助程式設計、型別系統、測試框架。他認為我們正朝著一個未來前進：程式碼重複表達意圖，並自動驗證一致性。隨著AI大量產生程式碼，系統自然會分為兩類：易受攻擊的邊緣模組與高度可信的安全核心。

真正的機會在於將形式驗證的努力集中在關鍵系統上——區塊鏈協議、作業系統核心、失敗會引發連鎖反應的部分。這才是投入產出最大化的地方。不是要證明所有東西，而是策略性地強化其他一切依賴的基礎設施。

這關於形式驗證採用與零知識證明整合的消息，反映出行業在安全性上的成熟。若你關注協議層的發展，值得留意。