The Ethereum Foundation’s Formal Verification team has launched better.codes with Yukon and zkSecurity. The challenge takes a specific problem involving Reed-Solomon codes and asks participants to improve its formally proven soundness bound.
Submissions are checked by the Lean kernel. The project makes accepted mathematical work available for subsequent participants to build on, rather than relying only on an informal argument that a result seems plausible.
The problem is relevant to hash-based succinct proof systems. The announcement distinguishes bounds researchers expect to hold from bounds they can currently prove. Progress on this challenge addresses that gap; it does not establish the security of every application that uses a related proof system.