Formal Verification of the INTMAX2 Protocol | Denisa Diaconescu (Nethermind)

Denisa 代表 NetherMind 向大會介紹了 Inmax 2 這個創新的以太坊擴容方案。Inmax 2 是基於 Validium Rollup 架構的解決方案，其核心創新在於突破傳統區塊鏈共識的束縛。與大多數 Rollup 方案不同，Inmax 2 不需要依賴底層共識協議驗證交易有效性，只需在 L1 合約中記錄操作順序。這種設計使得區塊構造者可以完全無狀態地工作，不需要維護系統狀態或選舉領導者，任何人都可成為聚合器，從而實現天然的抗審查性。

從用戶操作角度看，Inmax 2 定義了三類基本操作。存款很直接——用戶在 L1 合約向對應的 L2 地址發送資金，這筆資金被存儲在合約中。轉賬則是設計中最有趣的部分，分為兩個階段。首先，用戶選擇一個聚合器，然後發送一批交易，聲明要發送多少參與者和多少代幣。聚合器構建 Merkle 樹並生成證明，用戶簽名確認後，聚合器收集多個有效簽名並將其聚合後發布到 L1。其次，發送方需要將聚合器生成的 Merkle 證明發送給接收方。提現則需要先參與轉賬協議，將金額轉賬到 L1 賬戶，然後使用之前生成的證明觸發提現。

Inmax 2 之所以能實現如此高效的設計，關鍵在於一個巧妙的數學結構——拉蒂斯有序群構成的余額函數。在這個系統中，用戶負責維護自己的交易證明，但由於用戶可能只持有部分交易信息（尤其是當其他賬戶向其轉賬時），余額函數的設計必須能在信息不完整的情況下仍然防止雙重支付。拉蒂斯有序群提供了這樣的能力——它不僅允許代幣累加，還支持比較操作但無需全序關係，這意味著可以存在無法比較的代幣種類。最關鍵的是，余額函數會自動取提取金額與計算出的賬戶余額之間的最小值，這確保了即使在部分信息的情況下，用戶也無法超支。

為確保這一設計的數學正確性，NetherMind 團隊使用 Lean 4 對 Inmax 2 白皮書進行了形式化驗證，投入了約 3300 行精簡代碼。這項工作證明了一個核心的安全屬性：如果每次提款都成功完成，那麼 Rollup 合約就是安全的。破壞這個性質等同於破壞雜湊函數或簽名方案的正確性，這為整個協議提供了堅實的數學保證。

在性能方面，Inmax 2 聲稱鏈上數據只需 5 字節，這是通過精心設計的數據結構實現的。在當前以太坊區塊大小限制下，協議可支持每秒 7500 筆交易。但這裡有個巧妙的轉折——一筆「交易」在 Inmax 2 中實際上代表一批操作，單個發送方可向多個參與者發送任意數量的轉賬。因此如果以太坊未來增加區塊大小，Inmax 2 理論上可達到 Visa 級別的交易吞吐量。