Фонд Ethereum запустил вызов better.codes, продвигая доказуемую безопасность хэширования SNARK

Сообщение ChainCatcher, что команда формальной верификации Фонда Эфириума в сотрудничестве с Yukon и zkSecurity разработала открытую автоматизированную исследовательскую задачу better.codes, которая теперь доступна. Платформа формализует самосодержащие проблемы из Proximity Prize в Lean и помещает надежность машинной проверки koalaIRS12 в публичный рейтинг, чтобы любой мог способствовать улучшению, продвигая основанные на хэшах SNARK и постквантовые связанные с Эфириумом стандарты безопасности.

Решатели могут использовать свои AI-агенты для доказательства более высокой нижней границы надежности по этой задаче соседства Рида-Соломона, приближаясь к фиксированной цели в 128 бит. Ядро Lean проверяет каждую подачу, и повышенные доказательства улучшат публичную границу, а новые леммы, методы доказательства и результаты невозможности будут синхронизированы вверх по потоку, чтобы все участники могли их повторно использовать. Большинство хэш SNARK в производственной среде зависит от связанных промежутков соседства и связанных соглашений, и в настоящее время доказанные результаты все еще ниже, чем доверительные стандарты исследователей; эта задача направлена на то, чтобы открытым, инкрементальным и проверяемым образом сократить этот разрыв.

koalaIRS12 основан на соответствующей статье и формализован от начала до конца в ArkLib. Участники могут войти через GitHub и клонировать репозиторий задачи, подавая заявки в рамках фиксированных утверждений теорем и верификационной структуры; результаты, подтвержденные компаратором и ядром Lean, записываются в публичный репозиторий с указанием решателя и используемой модели. Сегодня запущен вызов на повышение надежности koalaIRS12 до 128 бит, в дальнейшем могут быть добавлены дополнительные задачи, детали будут определяться условиями проекта.