Verify a multi-step reasoning chain and return a Prova certificate summary.

Use this on any draft chain-of-thought before producing a final answer. A VALID verdict means the argument is structurally sound (no circularity, no contradiction, no unsupported leap). An INVALID verdict tells you exactly which step is broken in the failure field — repair that step and re-verify.

Args: reasoning: The reasoning chain as plain text (numbered steps or prose). retain: If True, the original reasoning text is persisted on the certificate row. Default follows PROVA_DEFAULT_RETAIN env var (False if unset). source_url: Optional URL of a paper or document this reasoning came from — surfaced on the certificate page. domain: Optional hint: medical | legal | financial | code | general. Improves failure-classification accuracy. metadata: Optional caller-defined key/value pairs (<=20 keys, <=8 KB) attached to the certificate.

Returns: Compact certificate summary including verdict, confidence_score, certificate_id, certificate_url, and (if INVALID) a failure block pinpointing the broken step.

Fetch a previously issued certificate by ID (e.g. PRV-2026-A7X4).

Returns the same compact summary as verify_reasoning. Use this to re-check a verdict, share a link, or inspect a failure that someone else's pipeline produced.

Download the self-contained Lean 4 proof for a VALID certificate.

INVALID certificates do not have a proof — the call will return an error. The returned lean_source can be passed straight into kernel_check_proof to verify it on the local machine without trusting Prova.

Returns: {certificate_id, lean_source, byte_count}

Run the Lean 4 kernel on a proof string locally.

This is the trust-anchor: Prova's verdict is only as strong as its server, but lean on the local machine is independent. Exit code 0 means the kernel accepted every step of the proof. Anything else means the proof is wrong and the certificate must not be trusted.

Requires the lean binary on PATH (override with PROVA_LEAN_BIN). Install via elan: https://github.com/leanprover/elan

Returns: {accepted, exit_code, stdout, stderr, lean_binary, lean_version}

Verify reasoning, then locally kernel-check the emitted Lean proof.

The complete trust loop in one call. If the verdict is VALID, the Lean proof is downloaded and handed to the local Lean kernel; the result tells you whether the proof is mathematically sound on your own machine, not Prova's. INVALID verdicts skip the kernel step and return the failure.

Returns: {certificate, kernel_check} — kernel_check is null when verdict != VALID or no proof was emitted.