LeanVM 以極簡虛擬機聚合簽章，探索以太坊抗量子方案

值得記下的 5 件事

1. [1:20]
   雜湊式替代方案仍有體積與聚合難題 講者提出以 SPHINCS 替換交易簽章、以 XMSS 替換共識簽章，並用編碼搭配雜湊樹處理資料可用性

   但這類簽章比現行方案大，也不具備 BLS 的原生聚合能力，需要另外處理大量簽章帶來的資料負擔。

2. [7:00]
   以遞迴證明分散簽章聚合工作 他提出用 STARK 證明大量簽章已通過驗證，讓區塊不必放入全部簽章

   各委員會可先產生證明，再由另一份證明驗證並合併；這種遞迴方式可讓聚合工作平行進行，而非全部集中交給單一聚合者。

3. [8:00]
   六項指令著重降低遞迴成本 LeanVM 的指令涵蓋算術、雜湊與控制流程

   講者表示，它具通用運算能力，但主要針對簽章聚合與遞迴最佳化；保持指令集精簡，有助減少驗證自身證明時必須檢查的條件。

4. [10:00]
   優先追求簡單與安全，形式化驗證尚未完成 講者認為效能已足以支援目標用途，應優先改善證明系統的簡潔與安全，而非只追求額外速度

   他表示正以 Lean 4 進行形式化驗證，也就是用形式化方法檢查系統的數學性質；不能將相關陳述已受審查解讀為整體驗證完成。

5. [16:20]
   產生證明與驗證證明有不同運算需求 談到執行分工時，講者表示，共識驗證者可用少量處理器執行緒產生證明並聚合簽章，手機等裝置則可快速驗證證明

   這些是講者口述的效能主張，逐字稿未提供完整測試條件。