← Front page · Technical Notes & Checklists
Guides · Checked 7 November 2026Auditing Lean 4 formalizations & specification seams
Practical reference notes for security auditors, formal-methods engineers, and researchers reviewing Lean 4 proofs—covering kernel trust boundaries, vacuous hypotheses, native_decide, and AI-generated formalizations.
| Guide | What it covers | Read |
|---|---|---|
| Audit Guide · Kernel & Statement Review How to Audit a Lean 4 Formalization: Escape Hatches, Axioms, and Specification Seams | A practical checklist for auditing a Lean 4 proof repository: checking axioms, catching native_decide and implemented_by, replaying with leanchecker --fresh and nanoda, and testing specification seams. | Read guide → |
| Audit Guide · Vacuity Probes & Witnesses Vacuous Theorems in Lean 4: How Contradictory Hypotheses Pass the Kernel | How a flipped inequality or off-by-one bound in a Lean 4 theorem hypothesis makes the statement vacuously true, why the kernel accepts it without warning, and how vacuity probes catch it. | Read guide → |
| Audit Guide · Kernel Trust Boundary `native_decide` and `Lean.ofReduceBool`: What the Lean 4 Kernel Trusts | How native_decide works in Lean 4, why it adds the Lean.ofReduceBool axiom, and how @[implemented_by] or @[extern] can make a theorem unsound when paired with native_decide. | Read guide → |
| Audit Guide · AI-Generated Formalizations Auditing AI-Generated Lean 4 Proofs: Why the Statement Is the Whole Trust Surface | Lessons from the October 2026 ETH and deterministic factoring formalizations: when an LLM writes 35,000 to 152,000 lines of Lean 4, how to audit the statement, machine model, and crossover constants. | Read guide → |