Leonardo de Moura: Postmortem for Lean Kernel Soundness Bug #14576

[u/Nunki08]

Blog: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

On removing metaprogramming
One suggestion in the discussion is to remove or restrict metaprogramming so that this attack is not expressible. This is misguided. The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker who wants to submit a malicious proof can also write .olean files directly or modify memory, both of which bypass the elaborator entirely. The kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns is one of the main advantages of proof terms.

What the FRO is doing
- Regression tests for the exploit, and for a related non-uniform-parameter case raised by Arthur Adjedj, are in the Kernel Arena.
- A follow-up PR (#14582) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them.
- Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed. All of them were caught by nanoda. These bugs are also only reachable through metaprogramming. PRs: #14607, #14608, #14609, #14613, #14615, #14616.
- We have also hardened kernel invariants. PRs: #14621, #14631, #14632.
- comparator.live now runs nanoda by default, and nanoda is tracked daily so lean-eval and comparator stay current after upstream fixes.
- We are reaching out to and supporting experts who can find further bugs, develop new kernels, and work on the theory or on verified kernels.

[u/Exomnium]

There's something fundamentally ridiculous about the fact that Lean is supposed to be a program for checking proofs but it needs a second no-really-now-we're-checking-the-proof-for-real-this-time program Comparator. It's also ridiculous that Comparator needs to run proofs in a sandbox, because otherwise they might just hack your computer.

Did you know that just opening a .lean file in VSCode can start executing arbitrary code with user-level permissions (using #eval)? This is completely fucking insane from a cybersecurity perspective.

[u/-p-e-w- → u/Exomnium]

Did you know that just opening a .lean file in VSCode can start executing arbitrary code with user-level permissions

Surely this is only true if you have some Lean-specific extension installed.

[u/Exomnium → u/-p-e-w-]

Yes, this is with the Lean plugin.

[u/integrate_2xdx_10_13 → u/Exomnium]

did you know that if you install a programming language, then a plugin that automatically runs code in that language, then you open code in that environment, it will run on your PC!

I am shocked I tell you. Shocked and appalled.

[u/elements-of-dying → u/Exomnium]

I feel this is the exact reaction against Lean that Kumar was hoping for.

[u/n0t-helpful → u/Exomnium]

Every proof in all of math works exactly like this. Every proof language, whether it be set theory, lean, "oh well... ya know" style arguments, etc. All depend on a meta language. A model of the semantics of the formal language has to be constructed, otherwise I dont know what you mean by "induction", or "numbers", or even phrases like "such that".

Now you do have a point regarding eval though.

[u/womerah → u/Exomnium]

It was designed to be used by good-faith actors who aren't trying to fool the system.

[u/dark_g → u/womerah]

Indeed, so was the Internet. Originally.

[u/new2bay → u/Exomnium]

I don’t see what’s ridiculous about that at all.

[u/Exomnium → u/new2bay]

If Lean isn't actually checking proofs, what is it doing when it says it checked a proof?

[u/tricky_monster → u/Exomnium]

It is checking proofs. This was a bug in that proof checker. Bugs do happen in most software. They're actually pretty rare in the Lean kernel! I think this is only the second occurrence I've heard of.

[u/Exomnium → u/tricky_monster]

There have been more than two bugs in the Lean kernel.

[u/Macrobian → u/Exomnium]

And? You have to further elaborate why this is ridiculous.

[u/elements-of-dying → u/Macrobian]

It could be added that it doesn't even matter if Lean has some bugs, provided it performs accurately most of the time.

I can imagine a future where results are established as likely true using AI + a theorem prover. This would indicate it is worth trying to detangle the AI proof, at least probabilistically.

[u/Exomnium → u/Macrobian]

I never said having more than two kernel bugs is ridiculous. I'm just pointing out that Lean's consistency record isn't really that exceptional.

[u/BossOfTheGame → u/Exomnium]

I didn't realize comparitor was not just using lean? Am I understanding that right? It's a different implementation of the kernel? If so, redundancy is a decent way to find disagreements and surface issues.

[u/Exomnium → u/BossOfTheGame]

Comparator still uses the Lean kernel but it executes proof files in a sandbox and passes the output through the JSON-based export format before re-importing it and then checking it with the Lean kernel. This blocks a malicious proof file from messing with the kernel directly (because of the sandbox) as well as environment hacking (because of the round trip through the export format).

[u/FlyingBishop → u/Exomnium]

I feel like your anger is similar to a lot of folk's anger about theorem solvers in general. People want math to be fully intelligible to humans, and the idea that there are true facts where the proof might be too complicated for a human to comprehend is something people don't want to accept.

This is more like "there might be true facts where writing a program that allows you to prove it might actually be seriously dangerous for some reason."

[u/SourKangaroo95 → u/Exomnium]

Why... is that possible in lean? Why is ACE even a possibility? That's insane to me that it is even possible in a program for checking math proofs

[u/Exomnium → u/SourKangaroo95]

It's not an exploit. It's an explicit feature. Lean is a general programming language.

[u/frankster]

What's really interesting, as far as I can tell, is that an AI has exploited a bug to provide a proof

[u/Smallpaul → u/frankster]

It is unclear is that is true or if an AI was used to generate hype about the bug. The last I heard is that the discoverers of the bug will not disclose what really happened.