Postmortem for the Kernel Soundness Bug Hunt — Leonardo de Moura

Leonardo de Moura

Postmortem for the Kernel Soundness Bug Hunt

2026-08-24

This is a follow-up to Postmortem for Kernel Soundness Bug #14576. We describe the kernel soundness bug hunt using OpenAI internal models, the new bugs found, and the actions the Lean FRO is taking to increase trust.

We are deeply grateful for all the help provided by Daniel Selsam at OpenAI. Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime. The collaboration with Daniel started on July 30 and was concluded on August 20, when the internal AI reported it could not find additional issues. Some of the bugs found by the OpenAI internal model have already been reported in the previous postmortem, but we repeat them here to ensure this document is self-contained.

The chapter Validating a Lean Proof from the Lean Reference Manual explains how potentially adversarial developments should be checked. lake build does not protect users from adversarial proofs that try, for example, to corrupt memory using Lean extensions. The gold standard is comparator and external checkers when you want to protect against a seriously malicious proof that compromises how Lean interprets a theorem statement or the user's system. We consider AI-generated proofs a potential source of malicious proofs.

On August 11, we wrote a document to assist the OpenAI internal model and other groups trying to find additional bugs in Lean kernels. This document was included in the prompt provided to the AI agents. It explains how to use tools such as comparator and external checkers, and instructs the agents not to spend time trying to corrupt memory by misusing Lean APIs or using unsafe code blocks, since these exploits are all caught when the proof is exported and rechecked. comparator was built to address this kind of exploit. We updated the document twice, on August 15 and 18, to describe additional exploits that are caught by comparator (e.g., an invalid prelude), and to explain that the 32-bit version is no longer supported. None of the groups using publicly available models reported any bugs.

At the end of the bug hunt, the OpenAI internal model focused on bugs in the Lean runtime. It found two very clever exploits. First, it found a way to overflow the reference counter of a Lean object used by the kernel, corrupt the memory, and then prove False. Second, it figured out that the official Lean distribution for Linux was not using the latest GMP v6.3.0, but v6.1.2, which contains a known bug, and crafted a proof of False exploiting this bug.

On August 21, we released Lean v4.33.1 with bug fixes for all issues found during the kernel bug hunt.

New Soundness Bugs

In this section, we cover pull requests (PRs) that fixed soundness bugs in the official kernel code. The OpenAI internal model managed to exploit all of them to get the official kernel to accept a proof of False. While fixing the issues, we also checked whether nanoda and ind-models (see below) rejected the bogus proofs.

#14613: fix: recognize sorts as Prop up to universe normalization. Both nanoda and ind-models rejected the bogus proof.

#14616 fix: reject declarations naming the kernel's _nested auxiliary types. Both nanoda and ind-models rejected the bogus proof.

#14806 fix: make kernel is_def_eq caching order-independent. Both nanoda and ind-models rejected the bogus proofs.

#14807 fix: make the kernel is_prop check require a sort and #14843 fix: apply #14807 fix to inductive.h. These two PRs fix the implementation of the function that decides whether a type is a proposition. The bogus proof was accepted by nanoda. lean4lean mirrors the implementation of the main kernel, but it does not have this bug, since its isProp already used ensureSortCore. ind-models rejected the bogus proof.

Runtime Soundness

In this section, we cover PRs that fixed bugs in the Lean runtime that were exploited by the OpenAI internal model to construct proofs of False that are accepted by the official kernel. Both bogus proofs are rejected by nanoda, and any other external checker not based on the Lean runtime.

#14838 fix: freeze objects when their reference count overflows. Previously, forcing a very large number of references to a single object wrapped the counter and corrupted the object's state; the object is now frozen (treated as persistent) and simply never freed, following the "sticky" approach used by the Koka programming language.

#14833 fix: require GMP 6.3.0. This is not really a bug in our source code. However, our Linux CI was constructing Lean binaries using GMP v6.1.2 for libc compatibility purposes, which contained a bug that could be exploited to construct a proof of False.

Other bugs

The following PRs do not fix soundness bugs. Some of them were exploits that were caught by our gold standard, but could also have been caught earlier.

#14607 fix: missing...