The kernel is the narrow trust point
A proof assistant can have a large parser, elaborator, tactic engine, compiler, editor, and package system. The final kernel has a smaller job. It checks whether the proof term follows the rules. A bug there can accept a false result.
Lean 4.35 turns an external recheck into a first-party command. lake check exports a development and checks it with leanchecker, which the Lean team describes as the official kernel without the surrounding system. The command runs in a sandbox by default.
Checker diversity helps when implementations fail differently. Count the independent failure paths, not the logos.
Paranoid mode has a concrete shape
lake check --paranoid adds nanoda, lean4lean, con-leche, and con-ron. The Lean team says this mode also runs an official-kernel variant with a hardened memory allocator. That allocator turns memory corruption into a checked abort instead of a silent wrong answer.
Those checkers do not all buy the same kind of separation. Con-leche is written in Lean and has a formal consistency proof relative to a set-theory model. That proof is checked by the official Lean kernel and assumes the consistency of the set theory used in the model. Con-ron is a Rust translation. Aeneas is used to prove that the Rust version refines the con-leche checking algorithm.
Different binaries can share one mistake
Two checkers can still share a specification, exporter, parser, compiler, runtime, big-integer library, build host, or fixture. A second green line means more when the second path has a different implementation and runtime. It means less when both lines reuse the failing layer.
The Lean post says con-leche checked a full Mathlib export in about 100 seconds with eight threads and used 0.69 times the instructions of the official kernel in that test. Read those as measurements from the published run. They are not a speed promise for another project or host.
Put the recheck after the build
lake check # Add the shipped independent kernels. lake check --paranoid # Keep the sandbox unless you have a reviewed reason not to. # lake check --inadvisably-no-sandbox
Save the Lean version, project revision, dependency lock, export digest, checker names, checker versions, exit codes, elapsed time, and stderr. A disagreement is a stop signal. Preserve the export and each checker output before rebuilding anything.
Do not call agreement absolute proof
Agreement says that the selected checkers accepted the same exported development under the recorded conditions. It does not prove that the exporter was correct, every dependency was the intended one, the host was clean, or the result applies to another revision.
The practical move is small. Add the default check to routine continuous integration. Run paranoid mode on release candidates or sensitive libraries. Keep the receipt. If the kernels disagree, stop the release and hand the saved export to the checker maintainers.