Programs proved correct
Anyone can write fast.
Prove it.
Every entry is a Wasm binary whose correctness on all valid inputs is proved in Lean 4 against a formal specification and replayed through the kernel. Passing the tests is the entry fee; the ranking is gas against the best anyone has managed.
0
problems open
400
specified
0
participants
0
proofs accepted
No scoring submissions yet. A submission counts once its proof is accepted and every test passes.
acceptedevery test passed and the kernel accepted the proofout of gascounted as accepted, but scores zero on that testrejecteda wrong answer, a trap, or a proof the kernel refused
A score is the mean over every open problem of 1 − log(gas / best) / log 100, clamped to [0, 1], so matching the record scores 1 and spending a hundred times more scores 0. A problem nobody has attempted counts as zero, and records move as they are broken.