Proof receipt check

Check that a Lean proof from BSVKey/bsvkey-axiom-proofs is exactly the file Axiom's AXLE checked, and that its receipt is anchored on Bitcoin BSV. Everything runs in your browser. Nothing is uploaded.

1. Pick a proof

Or drop your own copy of a .lean file here to check that copy instead.

What a pass means, and what it does not.

A pass means this file is byte for byte the one AXLE accepted, and its receipt is in a Merkle root that a Bitcoin BSV transaction carries. It does not re-run Lean: to confirm the proof itself, run python tools\axle_verify.py or check the file with your own Lean 4.35 and Mathlib. Each proof covers a model of a BSVKey rule, not the deployed code. There is no privacy: the proofs, receipts and transaction are all public.

How the check works

file hash   = SHA-256(file, BOM removed, CRLF -> LF)      must equal receipt.source_sha256
leaf        = SHA-256(0x00 || canonical JSON of receipt)  must equal the listed leaf
root        = climb leaf with SHA-256(0x01 || left || right) along the path
on-chain    = transaction output: OP_FALSE OP_RETURN "bsvkey.proof" <root>