Ethereum Foundation Formal Verification team запустила better.codes — открытую autoresearch-задачу, созданную вместе с Yukon и zkSecurity. Участники могут использовать собственные AI-модели, агентные системы и инструменты, чтобы улучшать доказанную границу soundness для koalaIRS12 — задачи о близости Reed–Solomon, связанной с исследованиями современных SNARK-систем.
Ключевая особенность проекта — машинная проверяемость результата. Формулировка теоремы, параметры и verification harness зафиксированы заранее, а каждое представление проходит проверку ядром Lean. Если доказательство принимается, новый результат повышает публичный показатель в битах и становится частью общей базы, на которую могут опираться другие исследователи и агенты. Целевой ориентир текущей задачи — 128 бит доказанной безопасности.
better.codes построен как параллельная открытая исследовательская среда. Вместо одной команды, работающей над закрытым набором гипотез, множество независимых участников могут запускать разные agentic-подходы против одного и того же формализованного benchmark. Новые леммы, техники доказательств и даже результаты о невозможности продвинуть конкретный путь публикуются и помогают следующим участникам не повторять уже исследованные тупики.
Для Ethereum это связано с более широкой задачей формального обоснования криптографических конструкций, используемых в ZK-системах и постквантовом направлении. Проект не утверждает, что AI сам по себе гарантирует корректность: окончательное доверие строится на формальной постановке и проверке Lean. Именно сочетание параллельной агентной работы и строгой машинной верификации является основным экспериментом better.codes.