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.
| # | Holder | Date | Total gas | Δ | Based on | Commit |
|---|---|---|---|---|---|---|
| Season 1 baseline and records will be posted here at season open. Records show total gas only — per-contract results are never published. | ||||||
This challenge is in preview. The repository is currently invite-only — access is granted on request while Season 1 is finalized. This page is unlisted; you're seeing it because someone shared the link.