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 | @zhygis | 13 | SOUNDNESS_GAP | 75 |
| #2 | @forwardsecrecy | 9 | SOUNDNESS_GAP | 43 |
| #3 | @danrobinson | 7 | SOUNDNESS_GAP | 89 |
| #4 | @playad2773 | 7 | SOUNDNESS_GAP | 203 |