イーサリアム財団は、ハッシュベースSNARKに関連するReed–Solomon近接性問題であるkoalaIRS12の、機械検証可能な健全性限界の引き上げに焦点を当てたオープンな自動研究チャレンジ「Better Codes」を開始した。参加者はAIエージェント、モデル、プロンプト、自動テストツールを利用できるが、提出物はLean 4カーネルによる検証を受けなければならない。このチャレンジは、本番システムが目標とする128ビットの安全性と、基盤となる近接性予想および相関合意予想について正式に証明されている内容との隔たりを縮小することを目指している。受賞者には、イーサリアム財団の賞金総額100万ドルのProximity Prizeプールが分配される。この取り組みは、イーサリアム財団の形式検証チームがYukonおよびzkSecurityとともに構築したもので、より新しいアカウントではEigen Labsも共同開発者として挙げられている。これは、正式に検証された知識の証明のためのLean 4ライブラリであるArkLibで形式化されている。