Skip to main content
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/. 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. 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:
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: Build:
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:
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 workflow. Windows runs through WSL.

​
See also