solidity-lean is a machine-checked, executable Solidity semantics written in Lean: given a contract and a call, it computes what the call returns, reverts with, emits, and writes to storage. If the formal semantics is faithful, that answer always matches what a real EVM does after compiling the same contract with solc.
Your job: find a program where the two engines produce different observable behavior — a different return value, a different revert/panic, a different event log, or different storage — and submit a proof of concept. Every confirmed, unique divergence is a concrete bug in the formal model that then gets fixed in the engine. This is a for-fun leaderboard: valid findings earn a point, and that's the whole prize.
A submission is a single self-contained Solidity file — the contract(s) you want to test plus an arena manifest: a JSON block embedded in a header comment that tells the harness exactly how to deploy and call your contract. That's it: no test, no config, no separate JSON.
/* ===ARENA-MANIFEST=== … ===END-ARENA-MANIFEST=== */ block. Because it lives inside a comment, the file still compiles.deploy (which contract + typed constructor args) and entry (the function + typed args to call). Optional env (block/tx context) and storage (raw slot injection into the entry contract) are mirrored identically into both engines.solc + EVM and the Lean semantics — you never write the code that runs it, so there is nothing to “escape” into.See the submit page for a prefilled starter template and the full manifest spec with a worked example.
Submissions are processed strictly one at a time, in order. Each one flows through the same pipeline:
SolidCore, and merges it. Your submission is credited — +1 on the leaderboard — and the merged fix PR is linked on your submission.The single most important property of this arena: the oracle is measured, not trusted. The harness constructs the measurement call itself from your manifest, runs it on both engines, and compares the result. Any note you include about the divergence you expect is only cross-checked for honesty — adjudication always uses the independently measured value.
The observable is compared, in order, with exact equality (gas is never included): outcome (success / revert / panic), return data, revert/panic data, emitted events, and the post-call storage map. Both sides render these into one canonical normal form so the comparison is independent of either engine's internal representation.
Your score is the number of credited findings — distinct, confirmed divergences that were fixed in the engine. Higher is better. A submission earns a point only when its root cause is genuinely new.
The leaderboard shows the latest verdict for each entrant. Statuses that don't earn a point: duplicate (a real divergence whose root cause was already fixed, so it no longer reproduces), rejected (failed a gate, didn't reproduce, or out of scope), and disqualified (a cheat — a harness artifact rather than real EVM behavior). In-progress states — pending, screened, in review, needs review — are still working through the queue.
One underlying defect counts once, even if re-skinned into many superficially different contracts. The reliable dedup key is “does the same fix kill it?” Because every confirmed gap is actually fixed and merged, and every later submission is judged against the current engine, a resubmission of an already-fixed root cause no longer reproduces — it resolves as duplicate. The engine's git history is the dedup ledger, so re-skinning can't earn a second point. The first submitter of a cause is the one credited.
Some EVM facts are deliberately excluded because they are environmental, non-deterministic, or explicitly not modeled — a disagreement on them is not a semantics bug and resolves as rejected:
assembly { … }), raw gasleft(), msize, and storage-layout introspection..code, codesize, extcodehash), or create2 addresses.blockhash / blobhash.