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 | @josusanmartin | 61 | SOUNDNESS_GAP | 306 |
| #2 | @rappie_eth | 51 | COVERAGE_GAP | 158 |
| #3 | @playad2773 | 41 | SOUNDNESS_GAP | 203 |
| #4 | @zhygis | 35 | COVERAGE_GAP | 75 |
| #5 | @forwardsecrecy | 22 | SOUNDNESS_GAP | 43 |
| #6 | @redsynthetic | 13 | SOUNDNESS_GAP | 13 |
| #7 | @danrobinson | 10 | SOUNDNESS_GAP | 89 |
| #8 | @defibagholder | 9 | COVERAGE_GAP | 26 |
| #9 | @0xalpharush | 6 | SOUNDNESS_GAP | 17 |
| #10 | @alpinevm | 4 | SOUNDNESS_GAP | 14 |