Make the edit.
Check the claim.
Change a small program. An agent proposes the existing add-chain pass.
Lean checks the proof against the actual Wasm bytes.
Same input.
Same behavior.
Live Lean kernel check and replay.What exactly do we prove? ↓
Read the agent’s plan
The plan is not proof authority. Only a successful Lean check, axiom audit and replay can produce an equivalence result.
Read the generated Lean proof
Read the checker log
Use the existing proof.
Check this exact edit.
The first example changes (x + 3) + 4 into x + 7. It uses Silmaril’s existing add-chain pass and its proved byte-processing contract.
The small C-style input is converted to readable Wasm text. Silmaril’s wasm-as produces the actual binary files. This input conversion is not a general C compiler.
The agent proposes the supported add-chain pass. Silmaril’s wasm-opt runs it. The candidate must match its output; unrelated edits are not automatically certified.
The generated proof contains the exact binary bytes. Lean discharges the successful-pipeline and candidate-matching obligations, then applies Silmaril’s existing soundness theorem. The resulting proof object is replayed with leanchecker.
Exact claim, supported edits and trust boundaries
The checked claim says the exact two byte arrays encode valid Wasm modules with ExportEquiv under Silmaril’s closed-host model, at every same numerical profile. This covers the modeled export observations, including repeated function calls. Timing and resource use can differ.
The input UI supports one uint32_t compute(uint32_t x) function with constants, parentheses, addition, subtraction and multiplication. It defines wrapping i32 arithmetic. It is not a full ISO C frontend. The proof starts at the resulting Wasm bytes, so it does not verify this C-style conversion.
Positive proofs currently require the candidate to match an existing selected Silmaril pass. This is not an automatic prover for arbitrary edits. A candidate mismatch, an unsupported edit or a failed proof is reported as “not established.” A browser execution counterexample is labeled separately; it is not a Lean theorem of inequivalence.
The proof uses public Silmaril revision 915988226ecd61a4862be0fadfdec89497592306, Lean 4.35.0-rc4, and only propext, Classical.choice, Quot.sound. No sorry, native_decide, custom arithmetic-checker fallback or new axioms are accepted. The library’s machine model, Lean toolchain, native runtime and I/O are trust boundaries.
The native tools run in bounded containers without network access. The website is on Cloudflare Pages; the native checker runs on the demo host. It can serve one native job at a time. A busy or unavailable service does not imply the programs differ.
Download Proof.lean and the recheck instructions to compile it against the pinned public library. The check record includes the binary hashes, exact claim, checker log, allowed axioms, object hash, library revision and elapsed time.