> ## Documentation Index
> Fetch the complete documentation index at: https://docs.certior.io/llms.txt
> Use this file to discover all available pages before exploring further.

# Live Lean verification

> Build certior-flow-check to add live per-plan flow verification on top of Certior's always-on Z3 gate.

The Certior runtime can route each plan through a Lean-checked flow verifier in addition to the always-on Z3 gate. This page explains what the binary is, why it is not shipped with the pip package, how to build it, and what the runtime does when it is present versus absent.

## What `certior-flow-check` is

A Lean 4 executable built from [`lean4/CertiorPlan/`](https://github.com/certior/certior/tree/main/lean4/CertiorPlan). It takes a JSON-serialised execution plan on stdin, type-checks each delegation step against the proven `Certior.Delegation` and `Certior.Encoding` lattice operations, and emits a verdict plus a Lean-issued proof certificate when the plan is admitted.

It is the live counterpart to the offline Lean proofs that run in CI. Both share the same source modules; the binary just runs the same model on a concrete plan rather than on the universal statement.

## Why it is not in the pip package

The compiled binary is \~93 MB. Shipping it inside the wheel would bloat `pip install certior` for every user, including those who never enable live Lean verification.

Without the binary, the runtime uses the Python implementation of the same subset and budget rule. Lean has proven that implementation sound offline. The behaviour is identical at the verdict level; only the source of the verdict differs.

## Installing the prebuilt binary (recommended)

`certior-install-lean` downloads the binary for your platform from the matching GitHub Release, verifies it against a SHA-256 baked into the pip package, and caches it where the runtime finds it automatically:

```bash theme={null}
pip install "certior[lean]"
certior-install-lean          # download + verify + cache
certior-install-lean --status # show install state, re-verify integrity
```

The download **fails closed**: if the binary's hash does not match the value shipped in the package, nothing is installed. Published platforms are Linux x86\_64 and macOS arm64; on any other platform the command reports that no binary is available and the runtime stays on the always-on Z3 path. The cached binary lives under `~/.cache/certior/bin/` (override with `CERTIOR_CACHE_DIR`), and the runtime discovers it with no env var to set.

## Building from source (alternative)

Requirements:

* Lean 4 toolchain (`elan` + `lake`). Install via [`scripts/install-lean-toolchain.sh`](https://github.com/certior/certior/blob/main/scripts/install-lean-toolchain.sh).
* The source repo cloned at the commit you want to attest.

Build:

```bash theme={null}
./scripts/build-lean-binary.sh
```

Produces the binary at `lean4/CertiorPlan/.lake/build/bin/certior-flow-check`. The script also runs the Lean test suite and `Certior.Audit` to confirm the four headline guarantees still depend only on Lean's three standard axioms.

## Enabling it at runtime

A binary installed with `certior-install-lean` is discovered automatically - no configuration needed. For a source build, point the runtime at the produced binary instead:

```bash theme={null}
export CERTIOR_FLOW_CHECK_BINARY=lean4/CertiorPlan/.lake/build/bin/certior-flow-check
./run.sh
```

The binary is resolved in order: `CERTIOR_FLOW_CHECK_BINARY` -> the `certior-install-lean` cache (`~/.cache/certior/bin/`) -> a local `lake` build -> `PATH`. When a binary is found and executable, Certior's **server-side plan-verification** endpoint uses it to machine-check submitted plans against the Lean model. The per-call SDK path (`Guard.verify()`) stays Z3-only — Lean's role there is the offline source fingerprint carried in every certificate, re-checkable with `lake build`. When the variable is unset or the binary is missing, plan verification degrades gracefully rather than refusing to start.

The OS support matrix mirrors the Lean 4 toolchain: Linux x86\_64 and macOS arm64 are tested by the [`lean-binary-ci.yml`](https://github.com/certior/certior/blob/main/.github/workflows/lean-binary-ci.yml) workflow. Windows runs through WSL.

## See also

* [Configuration](/reference/configuration) - the env vars governing the runtime.
* [How it works](/concepts/how-it-works) - the gates the binary participates in.
* [Trust package](/reference/trust-package) - the assurance the binary contributes to.