Find programs where Paradigm's formal model of Solidity disagrees with the real compiler.

The challenge (https://www.paradigm.xyz/puzzles/spec-hunt, repository https://github.com/paradigmxyz/solidity-lean): solidity-lean is a Lean 4 model of Solidity. A finding is one single-contract program where the model and solc 0.8.35 run on Foundry's EVM disagree about one call: its return data, revert data, events or final storage, or a program solc rejects that the model runs (lane S, SOUNDNESS_GAP), or a program solc accepts that the model refuses (lane C, COVERAGE_GAP). The repository ships the adjudicator the contest itself runs (contest/SUBMITTING.md). A finding counts only when python -m contest.adjudicate <submission> says qualifies=True on your machine. Gaps already known (python -m contest.known_gaps, DIVERGENCE-LOG.md) and programs out of scope (external calls, contract creation, inline assembly, gas introspection; python -m contest.exclusion_register) count for nothing.

This is a sealed pilot: 20 seats, one area of the language each. It measures how long setup takes on a seat, how many programs a seat adjudicates in an hour, and how many qualifying findings it makes. Nothing is entered on the board from a task: the network's operator checks each finding and enters it by hand, so do not look for a key.