How it works

Three steps. Every one of them checkable.

1. Submit the artifact

Paste Lean 4 code into the web verifier, POST it to the REST API, or call the verify tool on our MCP server. What you submit is hashed (SHA-256) the moment it arrives — that hash becomes part of the certificate, so the verdict can never drift away from the code it describes.

2. The engine checks the proof — for real

The verification engine runs the actual Lean toolchain (lake build) against your artifact in an isolated project. It is deliberately adversarial toward sloppy proofs:

Vacuous builds rejected. A target that compiles nothing is not a proof of anything.
sorry and admit rejected. Placeholders are not proofs.
Broken proofs rejected. If the toolchain reports an error, the verdict is FAILED, with the log attached.
Unfinished work reported honestly. Something that doesn’t compile yet gets INCOMPLETE — never a pass.

A pass means one thing: the toolchain compiled your artifact and the proof checked. The full transcript ships with the verdict.

3. The certificate seals the evidence

On PASSED, the certification authority issues a signed certificate containing:

Field	Meaning
`artifact_sha256`	Hash of exactly the code that was checked
`verdict`	PASSED, with the toolchain transcript reference
`toolchain`	Lean / lake versions that ran the check
`issuer`	AxiomCode CA
`serial`	Unique serial number
`validity`	90-day window (notBefore / notAfter)
`signature`	CA signature over all of the above

Check any certificate, no account needed: paste it into the certificate checker. You’ll get VALID, REVOKED, or EXPIRED — with the reason. Revocation is published, not hidden: if a toolchain bug ever invalidates a verdict, the serial goes on the public revocation list.

Interfaces

Humans: the web verifier and certificate checker.
Applications: the REST API with API-key auth and metering.
Agents: the MCP server — verify, check_certificate, pricing, usage_report. Plus llms.txt and machine-readable service info.