EthSystems завершила формальную верификацию приватного пула, охватывающую байт-код Sepolia

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

Этот контент предоставляется исключительно в общих информационных целях и не является финансовым, инвестиционным, юридическим или налоговым советом. Любые мероприятия, вознаграждения, онлайн-акции или связанная с ними информация, упомянутые в настоящем документе, не должны рассматриваться как рекомендация, приглашение к покупке, продаже, торговле или иной сделке с какими-либо криптоактивами. Криптоактивы очень волатильны и могут привести к убыткам. Доступность услуг, продуктов WEEX и связанных с ними событий может варьироваться в зависимости от региона. Вы несете ответственность за обеспечение того, чтобы ваше участие соответствовало применимым местным законам и нормативным актам.