A file goes in.
A hash comes out.
Run a small Linux program that computes SHA-256.
Then check Jad’s existing proof about its exact machine code.
Read the input.
Print its hash.
Exit 0.
Not just the input you try below.
Binary → model → proof → check.
- 1
Start with exact bytes
A fixed 35,512-byte x86-64 Linux executable. Its fingerprint identifies the file.
- 2
Read them in Lean
The proof checks the ELF file layout and uses Jad’s x86 and Linux execution rules.
- 3
State the output rule
The program must print the SHA-256 of its input, then two spaces, a dash and a newline.
- 4
Check the existing theorem
Lean checks a fixed entry point against the prebuilt public proof library.
Jad already wrote this proof. This page checks its entry point. The live C demo asks AI to write new proofs for your edits.
We send these UTF-8 bytes to stdin. No newline is added. Up to 16 KiB.
All permitted inputs. The same output rule.
The theorem proves the program does not fault or reach unmodelled behavior, writes the required hash, and finishes, under the model’s launch and I/O assumptions.
Uses prebuilt imports. This request does not rebuild or replay the whole proof library.
Read the Lean entry point
Read the checker log
A proof about
a real executable.
It covers machine instructions, reads, writes and process exit. It also proves agreement with a separately verified SHA-256 filter.
Change the executable and this proof no longer covers it. A new optimization needs a new proof.
What does “every input” mean here?
Every finite stdin admitted by the theorem’s launch conditions, including its input-length bound. It also accounts for permitted environment values, stack placement, undefined CPU flags, and read/write splits.
This page accepts 16 KiB of text for sample runs. That UI limit is separate from the theorem’s scope.
Is this GNU’s original binary?
This is sha256sum-min, a libc-free reimplementation of GNU coreutils 9.4’s stdin behavior. The pinned file has 35,512 bytes. It is not an unmodified distribution binary.
What do we trust? What is outside the proof?
We trust Lean’s kernel and its three standard axioms, the x86 and Linux models, and the chosen specification. Differential tests compare the x86 model with hardware; they do not prove the model equals the hardware.
File arguments, --check, I/O errors, signals, and inputs of 2⁶⁴ bits or more are outside this claim. Compiler correctness, execution speed and memory cost are not proved here.
The byte fingerprint is checked by the demo server. Lean checks the embedded ELF layout. This does not make the server’s file-hash calculation a Lean theorem.
What does the button check?
Lean checks a small file that states the fixed claim and applies Jad’s public theorem. It audits the claim’s axioms and rejects any dependency beyond propext, Classical.choice and Quot.sound.
The compiled imports were built in advance. The button does not replay all imported proofs. Download the instructions to build the public sources and run a full kernel replay yourself.
Download and check it yourself.
Public Silmaril source, pinned to one revision. No private library is needed for this example.