Команда формальной верификации @NethermindSec при поддержке @ethereumfndn через 2024 ZK Grants Round разработала Halva: инфраструктуру для формальной верификации zk-цепей Halo2 в @leanprover. Мы использовали Halva, чтобы выявить критическую ошибку в реальной цепи Scroll zk. 🧵 1/
5,09K