Как стало известно WuShuo, компания EthSystems, занимающаяся разработкой инфраструктуры для обеспечения конфиденциальности в Ethereum, опубликовала результаты формальной верификации пула конфиденциальных средств (Shielded Pool). Область проверки охватывает спецификации протокола, схемы доказательств с нулевым разглашением и байт-код контрактов, развернутых в тестовой сети Sepolia. Команда использовала такие инструменты, как Lean, Halmos, Kontrol, Aeneas и Verus, для многоуровневой проверки, направленной на предотвращение двойных трат, обеспечение сохранности активов, а также проверку реализации смарт-контрактов и кошельков. В частности, предотвращение двойных трат и обеспечение сохранности активов уже были проверены машинным способом в модели Lean. В ходе исследования было выявлено в общей сложности 6 проблем, 3 из которых связаны с самими инструментами проверки, и 2 из них могут привести к тому, что инструменты будут ошибочно доказывать ложные утверждения. EthSystems заявила, что большая часть доказательств была сгенерирована ИИ-агентом, а затем поочередно проверена ядром Lean.