Verify Independently

Kernel-check a Prova proof in 5 minutes

Every VALID Prova certificate ships with a self-contained Lean 4 proof. You do not have to trust Prova, Anthropic, or anyone in the pipeline. Download the proof and hand it to the Lean kernel — if the kernel accepts it, the argument structure is sound. If it rejects, the proof is wrong. There is no third option.

This is the entire trust model. Everything else on this site is convenience.

1. Install Lean 4

The easiest path is elan, the toolchain manager. It installs the same version the Prova emitter targets.

macOS / Linuxbash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source $HOME/.elan/env
lean --version  # lean 4.x.x

Windows: grab the installer from elan releases.

2. Download a proof

Open any VALID certificate and click download .lean. Or fetch it directly:

curlbash
curl -O https://api.prova.cobound.dev/certificate/PRV-2026-A7X4/lean
# → prova-PRV-2026-A7X4.lean

3. Kernel-check it

Hand the file to lean. Silence is success — the kernel exits 0 only when every step typechecks.

terminalbash
lean prova-PRV-2026-A7X4.lean
echo $?   # 0 means accepted

# Or use the built-in helper:
prova verify-proof prova-PRV-2026-A7X4.lean

Exit codes from prova verify-proof:

  • 0 — proof accepted, the argument is structurally valid
  • 1 — Lean kernel rejected the proof; do not trust the certificate
  • 2 — toolchain missing or I/O error

4. What the proof actually proves

Each file encodes the certificate's argument graph as a Lean DAG and proves two dual statements:

  • acyclicity — no claim circularly depends on itself
  • topological ordering exists — concrete witness via Kahn's algorithm

Both are checked by native_decide, which compiles the statement to an executable decision procedure. There are no sorrys and no added axioms beyond Lean's core — the emitter's output pins this at the top of every file with #print axioms.

5. What it does NOT prove

Structural soundness is not factual accuracy. Prova cannot tell you whether a premise is true — only that the conclusion follows from the premises as stated. A perfectly kernel-checked proof with "the sky is green" as a premise is still valid reasoning, just starting from a false claim. Treat the verdict as a lower bound on trust, not the ceiling.

Why this matters for auditors

A regulator does not have to take Prova's word for anything. They download the proof that was emitted the day the decision was made (the Lean file is stored on the certificate — it cannot be rewritten without breaking the SHA-256), install Lean, and re-run the kernel themselves. If it passes, the claim holds. If it fails, the certificate is void and Prova is liable. That is a defensible audit trail in a way "our tool said it was fine" never will be.