How it works

The challenge

Solidus is a formally verified Solidity/Yul → EVM bytecode compiler. A single Lean 4 theorem, Solidus.compile_correct, connects the source program's semantics to the emitted bytes on a pinned EvmYul interpreter. Your job: make the compiled contracts cheaper — deployment plus runtime gas, as aggressively as you like — while the theorem still proves.

Because the correctness claim is a machine-checked theorem over a frozen specification, there is no “did you break something” review step. If your compiler builds, the axiom audit is clean, and the frozen spec elaborates against it, your rewrite is correct by construction. Rewrite any pass, any IR, any internal proof — the theorem is the only referee.

The metric

One number: total gas to deploy and exercise a private test suite. For each contract, that is its deployment transaction plus a fixed set of private transaction vectors executed against it, on a pinned executor.

• Deployment gas prices bytecode size at the chain's real rate (200 gas/byte), so size-vs-runtime tradeoffs are priced by the metric itself rather than by a rule. There is no separate deployment-size cap: an oversized contract is penalised by the metric, not disqualified. Runtime byte counts and a >24576 flag are still reported, informationally.
• The vector mix (calls per deployment) plays the role of solc's --optimize-runs and is fixed per season.
• Record threshold: a submission takes the record if it improves on the current record by ≥ 0.1% (relative).

What is frozen

CI hash-checks these files, and the private scoring runner independently re-checks them from configuration you cannot touch. Submissions may not modify:

• the public entry point Solidus.compile? and the correctness theorems (Defs.lean, Correctness.lean);
• the semantic framework the statement is expressed in — the Simulation modules, the Yul interaction semantics, and the assembly/open interpreter semantics modules;
• the EvmYul dependency pin and lean-toolchain;
• the CI workflow files and the evaluation harness.

Everything else — every compiler pass, every IR, every internal proof — is yours to rewrite. Internal proofs are implementation detail: restructure, delete, or replace them, as long as the frozen theorems still prove.

The proof gate

• lake build EvmCompiler.Verification must succeed.
• #print axioms on Solidus.compile_correct and Solidus.compile_correct_creation must report exactly [propext, Classical.choice, Quot.sound]. This mechanically excludes sorry, native_decide, and smuggled axioms.

How to enter

1. Fork the repo; branch from arena (the current record) or from any record-NNN tag — building on older records is allowed and encouraged.
2. Optimize. Iterate locally against the public examples/ corpus.
3. Open a PR targeting arena, stating which record you branched from (Based-on: record-NNN); CI verifies it by git ancestry.
4. Public CI runs the proof gate, the frozen-hash check, and the public corpus. When it is green, a maintainer labels the PR for private scoring.
5. The private runner (sandboxed, offline) re-checks the frozen hashes independently, re-runs the proof gate, compiles the private suite, and reports one number: total gas.
6. Beat the record by the threshold → your PR is merged to arena, tagged record-NNN+1, and you enter the leaderboard permanently, with the lineage of which record you built on.

Records publish total gas only, plus the delta and a commit link. Per-contract results are never published — this is deliberate, anti-overfitting design.

Language coverage note

Unbounded recursion is not supported, by design. A function whose recursion depth depends on runtime input has no static bound on its operand-stack requirement, and the correctness theorem excludes stack overflow from the compiled code's possible behaviors — so no stack-headroom certificate can exist and Solidus.compile? fail-closes. This is a consequence of the guarantee, not a bug: Solidus refuses to emit code it cannot prove safe. Write recursive logic as loops.

The source of truth for these rules is CHALLENGE.md in the challenge repository.