Right exit code.
Still wrong?
A program can return 0 and still break its rule.
See the bug. Then check the proof that it is a bug.
Exit 0.
Write nothing.
Leave the file system unchanged.
Fix the rule. Compare the programs.
- 1
Keep the claim fixed
The program must finish with exit code 0 and no other observable event.
- 2
Choose exact machine code
Use the correct program, a wrong exit code, or an extra write.
- 3
Run a sample
Inspect stdout, stderr and the exit code. Each part matters.
- 4
Check the right theorem
Lean checks an existing proof of the rule, or a proof that the program breaks it.
A failed proof attempt does not prove a bug. The two broken examples have accepted proofs of the negative claim.
This program exits 0 and writes nothing.
exit(0);
Sample runs execute on the server. Lean checks a fixed entry point using prebuilt public imports; it does not replay the full library here.
Read the Lean entry point
Read the checker log
Prove the good.
Prove the bad.
The rule stays fixed. The correct program must meet it. A known broken program must be proved to violate it.
This is the basis of Jad’s verification tasks: reward checked reasoning about a fixed claim.
What do the three results mean?
Proved correct: the program meets the fixed rule at every permitted launch in the model.
Proved wrong: a Lean proof establishes that the program does not meet that rule. This is a proved counterexample, not merely a rejected positive proof.
Not established: the check failed, timed out, or was unavailable. It proves neither correctness nor a bug.
What does Lean prove for the bugs?
The wrong-exit theorem proves ¬ Total wrongExit trueSpec. The extra-output theorem proves ¬ Total extraOutput trueSpec.
The ¬ means “not.” These are proofs that the programs fail the original rule. Returning 0 alone is insufficient: stderr output also breaks the rule.
Can I edit these programs?
These are fixed examples with existing proofs. Their files and theorem names are pinned. Arbitrary edits need new proofs. Use the live C demo to try new edits within its supported Wasm subset.
What do we trust?
Lean’s kernel, the standard axioms, Jad’s x86 and Linux process models, and the chosen rule. The sample runs are separate Linux observations. Checking the entry point relies on prebuilt imports; the recheck script includes a full library replay.
Inspect the exact files.
Three programs. One rule. Public proof source pinned to one revision.