PANews, 27 октября: компания EthSystems, организация, занимающаяся разработкой технологий защиты конфиденциальности для институциональных пользователей Ethereum, объявила о завершении формальной проверки своего механизма защиты конфиденциальности, охватывающей все этапы – от письменной спецификации до байт-кода, используемого в тестовой сети Sepolia. Для проверки использовались различные инструменты на каждом уровне: Lean – для модели, схем и хеширования; Halmos и Kontrol – для контрактов; Aeneas и Verus – для кошелька; а также проверка восстановления байт за байтом для верификатора и развертывания. Двойное расходование средств и сохранение ценности были проверены с помощью машинных методов на основе теорем Lean. В ходе проверки было выявлено в общей сложности 6 проблем, 3 из которых касались самих инструментов проверки. Команда также перечислила предположения, на которые она по-прежнему опирается: устойчивость к коллизиям хеш-функций, то, что верификатор будет отклонять поддельные доказательства, и то, что контракты будут вести себя в соответствии с моделью.