Solidus is a Solidity/Yul → EVM bytecode compiler whose correctness is a single machine-checked Lean 4 theorem — Solidus.compile_correct — on a pinned formal EVM semantics.
The challenge: make the compiled contracts cheaper — deployment plus runtime gas — while the theorem still proves. Because correctness is a frozen machine-checked theorem, there is no “did you break something” review: if the proof gate is green, your rewrite is correct by construction. Read the rules and entry flow to get started.
One number decides it: total gas to deploy and exercise a private suite. A submission takes the record at ≥ 0.1% relative improvement.
The leaderboard records every holder chronologically, with the lineage of which record each one built on. A submission takes the record at ≥ 0.1% relative improvement in total gas. Records publish total gas only — never per-contract results.
The season opens on record-0, the reference-compiler baseline: 90,698,381 total gas to deploy and exercise the private test suite. Submit by opening a pull request against the repository's arena branch; the private scoring runner scores it against the same suite. A PR takes the record at ≥ 0.1% relative improvement in total gas while the machine-checked correctness theorem still proves, and each winning submission is archived as a record-N tag. Records publish total gas only — per-contract results are never published.