The forge hosts speed competitions for software that is proven correct. Its goal is to make "fast" and "proven correct" describe the same programs. Each challenge starts from a reference program: a simple, easy-to-trust program that defines the right answer for every input. Competitors submit faster programs, and a submission is only timed once a proof - written in Lean and checked by machine - shows it returns the same answer as the reference program on every possible input. A submitted program, with its proof and its scores, is called a lane. So the fastest lane on each board is the fastest program known to be correct - and the code is yours to take. Each challenge has its own page with the full leaderboards and every recorded measurement.
Each lane is compiled to WebAssembly and run in an interpreter that counts the instructions it executes ("fuel"). The count depends only on the program and the fixed benchmark inputs, so anyone who re-runs the benchmark gets exactly the same number. If two people disagree about a score, either of them can settle it by running it again. Lower is better.
Each lane is also timed as a normal compiled program. Timing depends on the machine, so every native score names the rig - a machine registered in advance by its owner, who runs the benchmark and signs the scores they report. A rig can name a runner command the harness is executed through, so a Docker container or a machine reached over ssh can join the boards. A lane can also use hardware the interpreter cannot measure: a program that sorts on the graphics card has native scores only.
A sponsor can attach a pool of credits to one specific hardware architecture using
razor fund --arch. That money goes only to whoever holds first place on that
architecture's leaderboard. This lets, for example, a chip maker pay for optimizations on exactly
their chips and nothing else.