縮小信任範圍：形式化驗證的規格、實作與以太坊進展

值得記下的 5 件事

1. [8:08]
   強化不變量，可能比直接證明目標更容易

   Sagiv 以球的移動為例：只要求「不會到達 D」，歸納假設仍容許從不可達的 B 走到 D；加入「也不會到達 B」後，較強的性質反而能證明。他表示，團隊已看到語言模型協助強化歸納假設的個別案例，尚未宣稱已能普遍自動完成。

2. [13:02]
   規格應在寫程式前開始，而不是完工後補上

   Sagiv 以 Aave V4 為例，說明先寫形式化不變量的做法；即使先用一般文字描述，也有助於釐清要求。依團隊使用前沿模型的初步觀察，模型較擅長把既有意圖轉成形式規格，真正困難的仍是人類先說清楚要保證什麼，這項判斷未來也可能改變。

3. [16:54]
   模型的證明成立，不代表實際執行的程式已獲驗證

   代理可能把複雜程式改寫成 Lean 模型，證出漂亮定理，卻未建立模型與原程式的對應。Sagiv 提醒，還要檢查驗證工具的可靠性、前提假設與規格是否正確；他採取直接驗證低階可執行程式的做法，但成本高，也有精化檢查等其他途徑。

4. [27:06]
   以太坊的驗證工作從電路延伸到虛擬機與密碼學

   Sorensen 將基金會工作分為零知識虛擬機電路、電路內的以太坊虛擬機（EVM）實作，以及底層密碼學規格。他介紹代理協助的低階 EVM 實驗，期待達成端到端驗證及速度、安全性領先；密碼學規格則已從精簡非互動式知識論證（SNARK）擴展到雜湊式密碼學。

5. [28:49]
   直接驗證低階程式，是縮小轉譯信任範圍的方向

   將 Rust 轉成 Lean 能支援既有程式庫的驗證，但仍須信任轉譯正確。Sorensen 預期，社群可在演講後約 6 個月開始取得可擴展工具，直接在 Lean 驗證各種編譯器產生的 RISC-V、x86 與 ARM 程式；這仍是開發方向與時程預測。