EthSystems完成隱私池形式化驗證，涵蓋規範到Sepolia位元組碼

PANews 10月27日消息，以太坊機構隱私技術機構EthSystems宣布對其隱私池（shielded pool）完成了形式化驗證，範圍從書面規範一直延伸到Sepolia測試網上運行的位元組碼。驗證按層使用不同工具：模型、電路和雜湊用Lean，合約用Halmos和Kontrol，錢包用Aeneas和Verus，驗證器和部署通過逐位元組重建核對。雙花和價值守恆已由Lean定理經機器驗證。驗證中共發現6個問題，其中3個出在驗證工具本身。團隊同時列出了仍然依賴的假設：雜湊無碰撞、驗證器會拒絕偽造證明、合約行為與模型一致。