EthSystems провела формальную верификацию приватного пула от спецификации до байткода на Sepolia
- —Верификация охватила модели, схемы и хеши (Lean), контракты (Halmos, Kontrol), кошельки (Aeneas, Verus)
- —Двойная трата и сохранение стоимости доказаны машинно в Lean
- —Найдено 6 проблем, 3 из них — в инструментах верификации
- —Остаются допущения: стойкость хешей и корректность верификатора
Почему важно: Формальная верификация приватных пулов снижает риск эксплойтов в анонимных трансферах и задаёт стандарт аудита для приватных L2-решений.
Источник: PANews