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 |
|---|---|---|---|---|---|---|
| 13 | @yevhenx33 | 2026-07-30 | 60,779,473 | −0.16% | record-12 | view |
| 12 | @josusanmartin | 2026-07-27 | 60,876,276 | −2.68% | record-11 | view |
| 11 | @demirelo | 2026-07-27 | 62,552,065 | −3.04% | record-10 | view |
| 10 | @josusanmartin | 2026-07-26 | 64,510,009 | −2.43% | record-9 | view |
| 9 | @noskillcoding | 2026-07-26 | 66,114,173 | −1.89% | record-7 | view |
| 8 | @demirelo | 2026-07-26 | 67,388,346 | −2.39% | record-7 | view |
| 7 | @Frodan | 2026-07-26 | 69,036,618 | −0.27% | record-5 | view |
| 6 | @Frodan | 2026-07-26 | 69,226,719 | −1.06% | record-4 | view |
| 5 | @demirelo | 2026-07-25 | 69,969,499 | −0.27% | record-4 | view |
| 4 | @dkuthoore | 2026-07-25 | 70,159,587 | −0.28% | record-3 | view |
| 3 | @noskillcoding | 2026-07-25 | 70,355,211 | −2.46% | record-0 | view |
| 2 | @josusanmartin | 2026-07-25 | 72,131,710 | −18.76% | record-0 | view |
| 1 | @yevhenx33 | 2026-07-25 | 88,787,921 | −2.11% | record-0 | view |
| 0 | Solidus reference compiler | 2026-07-22 | 90,698,381 | — | — | view |
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.