Lean 4 Soundness Bug #14576: What Broke the Kernel

During the week of July 27, 2026, the Lean 4 kernel accepted an axiom-free proof of False. The bug was not in the elaborator, not in user tactics, and not in a malformed .olean file. It lived inside the kernel's handling of nested inductive declarations, where a dropped phantom parameter escaped type checking. The Lean FRO had a fix within an hour of the report, and a week later the follow-up hardening campaign had already closed related paths and added regression tests to the Lean Kernel Arena.

This post walks through the mechanics of the bug, why an independent checker failed to catch it, and what it means for teams that rely on proof assistants for security work. All claims trace back to the official postmortem, the GitHub issue, and the merged fix.

The One-Sentence Version

A nested inductive type E was declared with an ill-typed projection inside its constructor. The kernel's elimination routine for nested occurrences dropped the parametric arguments of the nested type before checking them, so the bad projection was accepted. Once E was in the environment, a metaprogram built a theorem bad : T false from T true, and nomatch derived False with no axioms.

What Lean's Kernel Actually Does

In a dependently typed proof assistant like Lean 4, the kernel is the only trusted component. The elaborator, tactics, macros, and metaprograms are untrusted; their job is to produce a term the kernel accepts. If the kernel accepts a term of type False, the logic is broken, regardless of how many friendly frontends stand in front of it.

The kernel checks every declared inductive type, every definition and proof term, and every definitional-equality comparison. An attacker can bypass the frontend by writing a malicious .olean file or by using metaprogramming to call addDecl directly. That is why the kernel is the trust boundary, and why this is a kernel bug rather than a frontend bug.

Courtesy: Essam Mamdani / generated diagram. Source: derived from the Lean 4 architecture described in the official postmortem. Accessed: 2026-08-02. The diagram shows the critical separation between the untrusted elaborator and the trusted kernel. Soundness can only be guaranteed by the kernel itself; any check performed by the frontend is a convenience, not a guarantee.

The Bug: Phantom Parameters in Nested Inductives

Lean lets you define an inductive type T that contains a nested occurrence of another inductive type I. When the kernel processes such a declaration, it eliminates the nested occurrence I Ds is into one or more auxiliary types. The parameters Ds of I are abstracted away during this elimination because they are uniform across the recursive structure.

The problem: when the parameters Ds are phantom—meaning they do not appear in any constructor field of I—they are dropped entirely from the generated auxiliary type. Because they are dropped, they are no longer type-checked in the context of the new declaration. An ill-typed argument can therefore be smuggled through the elimination routine.

This is exactly what happened in the reported exploit. The declaration used a projection whose structure name did not match the value being projected. In ordinary surface Lean, the elaborator would reject it, but the declaration was submitted directly to the kernel through a metaprogram. The kernel's nested-inductive elimination did not re-check the dropped phantom parameter, so the declaration passed.

The kernel's type checker and definitional-equality routines also had a related gap: they compared projections by index and projected expression only, ignoring the structure name. The follow-up hardening PR (leanprover/lean4#14631) explains that this comparison was safe only as long as every submitted projection was well typed. Once the nested-inductive bug allowed an ill-typed projection into the environment, the projection comparison became an attack surface.

The Exploit: From Ill-Typed Projection to False

The reproduction in issue #14576 is short and self-contained. It declares a small family of types and then uses metaprogramming to build a declaration that the kernel should reject.

1import Lean
2open Lean Elab Command
3
4inductive P : Prop where | mk (b : Bool)
5structure C where b : Bool
6inductive W : Type where | mk (p : P)
7inductive L (α : Type) (b : Bool) : Type where | mk
8inductive T : Bool → Prop where | mk : T true

The key ingredients are:

• P is a proposition wrapping a Bool.
• C is a structure with a Bool field.
• W is an inductive whose only constructor takes a P.
• L is a phantom-parameter inductive: the parameter b does not appear in the constructor.
• T is a type family indexed by Bool, inhabited only at true.

The exploit then builds a nested inductive E whose constructor contains a projection of C applied to a value of type W. That projection is ill typed: W is not a C. Because the kernel's nested-inductive elimination drops the phantom b parameter of L and does not re-check the dropped argument, the bad projection is accepted.

Once E is in the environment, the rest is a chain of well-typed-looking manipulations that derive bad : T false from T true. Since T false is uninhabited, nomatch bad yields False. The final #print axioms reports no axioms, because none were used: the kernel itself certified the contradiction.

1theorem boom : False := nomatch (bad : T false)
2#print axioms bad
3-- 'bad' does not depend on any axioms

Courtesy: Lean Prover / GitHub. Source: https://github.com/leanprover/lean4/issues/14576. Accessed: 2026-08-02. The screenshot captures the issue title and reproduction, confirming that the bug was reported through the public tracker with a self-contained test case and that it affected checked-kernel soundness.

Why nanoda Did Not Catch It

nanoda, an independent Lean kernel written in Rust by Chris Bailey, is one of the main external checkers. It is intentionally separate from the official C++ kernel, so a bug in one should not imply a bug in the other. The Collatz proof that triggered the investigation had already passed a week-old version of nanoda.

The reason is sobering: two unrelated bugs lined up. The official kernel failed to check the dropped phantom parameters in nested-inductive elimination. nanoda did check that spot, but it failed to verify the structure name in a projection node. The exploit was constructed so that the expression the kernel never inspected was one that the old nanoda accepted. The result passed both checkers while being logically invalid.

This is a classic example of why independent verification is necessary but not sufficient. It also shows why two independent implementations can still fail together when the same adversarial input exploits two different weaknesses. The nanoda bug was reported by Jeremy Chen and fixed before the Lean bug was reported, so current versions of both checkers catch the exploit. The Lean FRO now tracks nanoda daily and runs it by default on comparator.live.

lean4lean, Mario Carneiro's project to formalize Lean's type theory and prove the kernel implements it, is also affected because its inductive handling is a port of the reference implementation. The postmortem notes that the bug would have been found when the verification work reached inductive types, but that part of the proof is still ongoing.

Courtesy: Lean FRO / Kernel Arena. Source: https://arena.lean-lang.org/. Accessed: 2026-08-02. The arena runs the same proof corpus through multiple independent checkers and records pass/fail/crash results. Regression tests for this bug and related non-uniform parameter cases are now part of the tracked corpus, making cross-checker divergence visible quickly.

The Fix and the Hardening Campaign

The fix in PR #14577 is small but precise: after the nested-inductive elimination generates auxiliary types, the kernel type-checks the dropped parametric arguments Ds against the post-declaration environment. This closes the gap where phantom parameters escaped scrutiny.

A follow-up PR (#14582) strengthened the check: instead of only re-type-checking the parameters, the kernel now verifies that the parameters of a nested occurrence actually behave as parameters. This catches a related non-uniform parameter case raised by Arthur Adjedj.

The hardening did not stop there. According to the postmortem, Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, which found additional programming mistakes in the kernel. These were reachable only through metaprogramming, were caught by nanoda, and were fixed in PRs #14607, #14608, #14609, #14613, #14615, and #14616. Kernel invariants were also tightened in #14621, #14631, and #14632.

The practical response is a good template for any project that ships critical core code:

Lessons for Proof Engineers and AI-Assisted Verification

The first lesson is about boundaries. A suggestion in the discussion was to restrict metaprogramming so the attack could not be expressed. The postmortem rejects this as misguided. The elaborator is untrusted by design, and soundness cannot depend on it refusing to build a bad term. An attacker can write .olean files directly or modify memory. The kernel must reject ill-typed declarations on its own. This is the same boundary thinking that applies to MCP tool servers or file upload pipelines: never trust the client; validate at the trust boundary.

The second lesson is about independent verification. Running a second checker is valuable, but not a guarantee. The nanoda and Lean kernels had different bugs that happened to complement each other. Teams that rely on formal proofs should understand the assumptions of their checkers and keep them current. A stale checker is a false comfort.

The third lesson is about AI-generated code. The original Collatz proof was produced with AI assistance. The model found a real kernel bug by constructing a proof that should not have existed. This is a reminder that AI-assisted security research is a double-edged tool: it can find genuine vulnerabilities faster than humans, but it can also produce misleading artifacts that exploit subtle weaknesses in verification infrastructure. The Lean FRO's collaboration with OpenAI to audit the kernel with a specialized AI is one model for doing this responsibly.

The fourth lesson is about verification coverage. lean4lean's proof of consistency does not yet cover inductive types, and the implementation under verification had the same bug as the reference kernel. A partially verified kernel is still partially unverified. Teams should track exactly which parts of their toolchain have machine-checked guarantees and which still rely on human review.

Production Checklist for Proof-Assistant Users

If your team depends on a proof assistant, this bug is a prompt to audit your assumptions:

• Know your trust boundary. The kernel is the only trusted component. Any check outside the kernel is a convenience, not a guarantee.
• Run an independent checker. Use nanoda, lean4lean, or another checker on your proof corpus, but keep it up to date and understand what it does and does not verify.
• Track regression tests. If your tool has a public test arena, monitor it for new failures and add your own critical proofs to it.
• Pin and upgrade carefully. Patch releases that fix kernel bugs should be applied promptly. A proof written against a buggy kernel is not a proof.
• Audit metaprogramming. Any code that calls addDecl or writes .olean files directly bypasses the frontend. Treat it as a privileged operation.
• Separate verification from compilation. Do not let build convenience blur the line between what the elaborator accepts and what the kernel checks.
• Model AI as a tool, not an oracle. AI-assisted proofs should be checked with the same rigor as human proofs, and the tools used to check them should be under continuous review.

FAQ

What is a soundness bug in a proof assistant?

A soundness bug means the kernel accepts a proof of something not actually provable. In this case, it accepted a proof of False with no axioms, which breaks the entire logical foundation.

How was this bug found?

Ramana Kumar published a repository containing an AI-assisted, sorry-free "disproof" of the Collatz conjecture. It was not a valid proof; it exploited the kernel bug. Kiran Gopinathan reduced it to a minimal proof of False and opened issue #14576.

Why didn't Lean's frontend stop the bad declaration?

The declaration was submitted directly to the kernel through metaprogramming, bypassing the frontend. The frontend would have rejected it, but soundness cannot depend on the frontend because an attacker can write .olean files directly or modify memory.

What is nanoda and why did it fail?

nanoda is an independent Lean kernel written in Rust. It failed because it did not check the structure name in projection nodes. The exploit was constructed so that the official kernel's weakness and nanoda's weakness aligned, allowing the bad proof to pass both.

Is this a flaw in Lean's type theory?

No. The postmortem explicitly states this is an implementation bug, not a hole in the meta-theory. The kernel's elimination routine for nested inductives simply did not re-check dropped phantom parameters.

Should I stop using metaprogramming in Lean?

No. Metaprogramming is a powerful and legitimate feature. The lesson is that the kernel must reject ill-typed declarations regardless of how they are submitted. Removing metaprogramming would not make the kernel safer; it would just remove a useful tool.

What should teams verify before trusting a proof assistant?

Teams should know the kernel's trust boundary, run independent checkers, track regression tests, apply kernel patches promptly, and understand which parts of the toolchain have formal guarantees.

Sources and Discovery Trail

• Discovery lead: Hacker News front page for August 1, 2026, item "Postmortem for Kernel Soundness Bug #14576" (https://news.ycombinator.com/front).
• Official postmortem: Leonardo de Moura, "Postmortem for Kernel Soundness Bug #14576," 2026-08-01. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/
• Issue tracker: leanprover/lean4, "Kernel accepts wrong-structure projections, allowing an axiom-free proof of False," #14576. https://github.com/leanprover/lean4/issues/14576
• Fix: leanprover/lean4, "missing check at kernel inductive declaration," #14577. https://github.com/leanprover/lean4/pull/14577
• Follow-up fix: leanprover/lean4, "Check that nested occurrence params behave as params," #14582. https://github.com/leanprover/lean4/pull/14582
• Independent checker: ammkrn/nanoda_lib. https://github.com/ammkrn/nanoda_lib
• Verification project: digama0/lean4lean. https://github.com/digama0/lean4lean
• Regression arena: Lean Kernel Arena. https://arena.lean-lang.org/
• Comparator service: comparator.live. https://comparator.live.lean-lang.org/
• Related reading: Essam Mamdani, "MCP Security Threat Modeling Guide," https://essamamdani.com/blog/mcp-tool-server-threat-modeling; "File Uploads: Threat Model and Controls," https://essamamdani.com/blog/file-uploads-threat-model-and-controls; "Secure AI Containers with SBOMs and Provenance," https://essamamdani.com/blog/secure-ai-container-supply-chain-sbom-provenance.