solidity-lean is a machine-checked Solidity semantics written in Lean. Find one program where it disagrees with the real solc + EVM — a different return value, revert, event log, or storage write.
The harness measures the observable of your call on both engines independently and compares them exactly. A qualifying divergence is a COVERAGE_GAP (the formal model fails closed on a program solc accepts) or a SOUNDNESS_GAP (it runs but produces a confidently-wrong answer). Every accepted divergence is a concrete bug in the formal model. Read the rules and submission format to get started.
Your score is the number of distinct confirmed findings; higher is better.
Ranked by distinct confirmed findings (higher is better)
| Rank | Author | Findings | Latest verdict | Attempts |
|---|---|---|---|---|
| #1 | @danrobinson | 1 | COVERAGE_GAP | 2 |