EthSystems завершила формальную верификацию privacy pool: от спецификаций до байткода Sepolia
chaincatcherEthereum-организация по технологиям институциональной приватности EthSystems объявила о завершении формальной верификации своего privacy pool (shielded pool) — от письменных спецификаций до байткода, работающего в тестовой сети Sepolia. Верификация использовала различные инструменты на разных уровнях: модели, схемы и хеши — Lean, контракты — Halmos и Kontrol, кошельки — Aeneas и Verus, а валидаторы и развертывания были проверены посредством побайтовой реконструкции. Двойная трата и сохранение стоимости были верифицированы с помощью теоремы-доказателя Lean. В ходе верификации было обнаружено в общей сложности 6 проблем, 3 из которых были найдены в самих инструментах верификации. Команда также перечислила допущения, на которые они по-прежнему опираются: устойчивость хешей к коллизиям, валидаторы будут отклонять поддельные доказательства, а поведение контрактов соответствует модели.
Данный контент предназначен исключительно для информационных и образовательных целей и не является инвестиционным советом, связанным с BTCC. BTCC прилагает все усилия, но не может гарантировать правдивость, точность или оригинальность вышеприведенного контента.