A Lean Use-After-Free That ‘Proves’ 1 + 1 = 3

On a vulnerable build of Lean, I could write a program with no unsafe declarations and have it accept a theorem claiming that (1 + 1 : Nat) = 3. The program used a memory-safety bug in Lean's native runtime to change the result of a computation that the proof relied on.

This is the theorem from the reproducer:

public theorem one_plus_one_eq_three : (1 + 1 : Nat) = 3 := by
  have nativeLie : @decide Target (forgeDecision 0) = true := by
    set_option interpreter.prefer_native true in
      native_decide
  exact @of_decide_eq_true Target (forgeDecision 0) nativeLie

Lean accepted it and reported:

'one_plus_one_eq_three' depends on axioms:
[propext, one_plus_one_eq_three._native.native_decide.ax_1_1]

native decision for 1 + 1 = 3: true

The generated native_decide axiom is part of the result. Lean's kernel checked a proof that depended on an assumption supplied by native evaluation. Memory corruption made that evaluation return the wrong answer, and the answer entered the theorem as an explicit assumption. The kernel did not independently derive false arithmetic.

Winfunc found the underlying use-after-free while scanning Lean. I reproduced it, reduced it, and reported it as Lean issue #15072. The initial report established a crash and explained how a stale reference could observe a replacement value. The proof-forging variant came later, after Trail of Bits published a different Lean bug that produced a very short “proof” of Fermat's Last Theorem.

Their result prompted a question about our finding: could this native memory-safety failure also change a proof decision? The theorem above answers that question, but understanding the answer requires following the value through the compiler, the runtime, and finally the proof's assumptions.

What native evaluation asks us to trust

Lean is both a programming language and a proof assistant. Those roles share infrastructure, but a successfully executed program and a checked proof offer different guarantees.

In the usual proof-checking model, tactics help construct a proof term and the kernel checks that term against the theorem statement. A tactic can contain a bug without making the kernel accept its invalid output. The kernel still checks that the conclusion follows from the declarations and assumptions available to it.

Native evaluation changes which assumptions are involved. A proof may depend on the result of compiled code because evaluating a large computation through ordinary reduction would be too expensive. The native compiler and the relevant runtime implementations then become part of the trusted computing base: the components whose correctness the result depends on.

Lean makes this dependency visible. Under the per-computation axiom design described in RFC #12216, a use of native evaluation introduces a dedicated axiom. In this example, its name is:

one_plus_one_eq_three._native.native_decide.ax_1_1

That name identifies the assumption introduced by native computation. It doesn't establish that the computation was correct. The distinction matters because the rest of a proof can follow correctly from an assumption that is false.

The reproducer contains no handwritten FFI, modified runtime, malformed .olean file, or fake compiler output. Its native code is generated from safe Lean source. The failure is in the implementation that should preserve that source's meaning and memory safety during execution.

The boundary bug

The underlying mistake was an off-by-one check at the boundary between the compiler's constructor layout and the runtime's object header.

A constructor's layout tells the runtime which parts of an object contain references to other objects and which parts contain scalar data. That information affects how the runtime copies an object, traverses its children, and manages their lifetimes. It has to agree with the layout used by generated code.

At the vulnerable revision, Lean's object header was defined as:

typedef struct {
    int      m_rc;
    unsigned m_cs_sz:16;
    unsigned m_other:8;
    unsigned m_tag:8;
} lean_object;

For a constructor object, m_other records the number of leading object-pointer fields. It has eight bits, so the largest count it can store is 255. The runtime expresses this limit using a constant:

#define LEAN_MAX_CTOR_FIELDS 256

Despite the name, 256 is an exclusive upper bound. The allocator's assertion makes the contract explicit:

assert(num_objs < LEAN_MAX_CTOR_FIELDS);

The compiler obtained the same limit from the runtime, but the IR checker treated it as inclusive:

if c.size > maxCtorFields then
  throwCheckerError s!"constructor '{c.name}' has too many fields"

A constructor with exactly 256 object fields passed this check. The compiler could therefore emit a call equivalent to:

lean_alloc_ctor(0, 256, 0);

In a Release build, the assertion did not stop the allocation. Lean allocated enough memory for the object: on the tested 64-bit build, an eight-byte header and 256 eight-byte pointer slots occupied 2,056 bytes. The generated field writes all stayed within that allocation.

The count still had to fit into the header. Storing 256 in the eight-bit m_other field retained the low eight bits, producing zero. The allocated object now contained 256 pointer fields while its runtime metadata described an object with no pointer fields.

This explains why checking the allocation size alone would miss the problem. The bytes existed and the initial writes were in bounds. The corruption affected the information that other runtime operations used to interpret those bytes. Meanwhile, the compiler retained the original layout and continued generating code on the basis that there were 256 fields.

From zero fields to dangling pointers

The contradictory counts became a use-after-free when an operation copied the object using the runtime header and generated code later destroyed the original using the static layout.

That operation was ShareCommon.shareCommon', a safe Lean function backed by the native lean_sharecommon_quick implementation. ShareCommon walks an object graph and produces a copy that reuses equal subobjects. To do that safely, it must distinguish references to child objects from scalar bytes and preserve the references needed by the copy.

The constructor visitor obtains the child count from the header:

unsigned num_objs = lean_ctor_num_objs(a);

For the 256-field object, this returned zero. The visitor still used the allocation's real byte size, so it treated the remaining 2,048 bytes as scalar data. It allocated a constructor with zero children and copied those bytes with memcpy.

The copy preserved the addresses stored in the fields, but it did not retain the referenced objects. A byte copy can reproduce a pointer's value without acquiring the ownership that makes the pointer safe to use. Here, the code responsible for retaining children ran zero times because the header said there were none.

The compiler later destroyed the original constructor. Its static layout information still specified 256 object fields, so the generated code used:

lean_dec_ref_known(original, 256);

That operation released the original's child references. Once the child's reference count reached zero, it was freed even though the ShareCommon copy still contained its address. A later projection such as shared.f000 remained valid Lean source, but native execution returned a dangling pointer.

The original reproducer stored a one-element Array Nat in the constructor's fields. The 255-field control printed got=41, fresh=42. The 256-field case crashed with SIGSEGV on my macOS arm64 Release build. If the allocator immediately reused the freed array's address, the stale field could instead observe the replacement value, 42.

The source analysis explains the ownership failure; the crash confirms that the compiled program reaches a memory-safety failure. Changing a proof decision requires the more specific behavior in which a stale reference reads a replacement value.

Making a dangling pointer say “true”

Lean represents a decision about a proposition p with Decidable p. An isFalse value contains a proof that p is false, and an isTrue value contains a proof of p. At the source level, those proof obligations prevent a program from treating a proof of one proposition as a proof of another.

During native compilation, proof values are erased. In the specialization used by this reproducer, the decision is represented by its constructor tag: zero for the false decision and one for the true decision. The native representation relies on compilation and execution preserving the meaning of the well-typed source.

The reproducer's target is:

public abbrev Target : Prop := (1 + 1 : Nat) = 3

It starts with the honest isFalse decision for that proposition, stored in a heap cell. All 256 fields of a Wide constructor refer to the same cell. After ShareCommon makes its malformed copy, generated reference-count code releases the original references and frees the cell.

The replacement allocations contain isTrue True.intro, which is a valid decision for the proposition True. At the source level, the original and replacement cells have different types:

Cell (Decidable Target)
Cell (Decidable True)

Their native cell layouts are the same. When a replacement occupies the address retained by the stale field, native execution reads its true tag through an expression whose static type still refers to Target:

shared.f000.value

The source expression promises a Decidable Target. The bytes at the dangling address now come from a Decidable True. The reproducer does not need to construct a source-level proof of the false proposition; it relies on memory corruption to break the correspondence between the source type and the native value.

The published reproducer allocates 65,536 replacement cells. That count is a heap-shaping parameter used to make reuse stable in the tested executable and native-evaluation process. The vulnerability boundary remains the constructor's 256 object fields.

The evaluation path also matters. Lean can interpret IR or call a precompiled native symbol, and this bug affects native execution. The Lake package sets precompileModules = true so that the trigger module is built as an exported native library and loaded while Main.lean is elaborated. The library contains C generated from the safe Lean module. Without that setting, the evaluator can take the IR path and return the honest false decision.

The theorem at the start of the article consumes the corrupted native result. Its axiom list records that dependency, which is why the accepted declaration must be read together with its assumptions.

How Winfunc found it

Winfunc's stored trace begins before the agent had selected the off-by-one check or ShareCommon as the relevant runtime operation. It first mapped Lean's compiler, runtime, exposed build paths, and trust boundaries. From that map, the planner created a bounded mission named constructor_layout_narrowing_boundaries.

The mission asked whether compiler layout values were consistently constrained before they reached compact runtime fields. Lean's compiler represents constructor counts as Nat, while the native header stores the corresponding object-field count in eight bits. That change in representation supplied a concrete invariant to investigate: every accepted count had to remain representable at runtime.

The stored candidate trace records the time and tool use for three stages:

These were read-only repository sessions. The agents searched code and read files; they did not build Lean or execute the reproducer. The trace documents how the finding was reasoned about. The later runtime work provides a separate kind of evidence.

Following the count across representations

The mission's initial searches covered constructor limits, layout indices, allocation functions, and header fields such as m_other. It connected the compiler's layout representation to the runtime header before settling on a particular consumer of the malformed object.

One of the relevant definitions was setCtorLayout, which increments a Nat count for each runtime object field. The agent followed that count through the compiler's intermediate representations, the C and LLVM emitters, and the interpreter. It found that the IR check allowed exactly the value that the native header could not represent.

At that point, the agent had identified inconsistent metadata. It still needed to establish a harmful consequence. A truncated count might lead to several possible behaviors, and the allocation itself was correctly sized. The mission therefore inspected consumers of dynamic constructor metadata, including reference-count destruction, multi-thread marking, compact regions, and ShareCommon.

ShareCommon supplied the missing relationship between the count and object ownership. Its visitor used the dynamic header to decide which fields needed reference handling. That gave the candidate a concrete memory-lifetime failure to investigate beyond the integer truncation.

Testing the counterarguments

The judge checked whether the candidate survived the obvious objections. Could the allocator assertion prevent it? Were the initial stores out of bounds? Did the program need forged compiler IR or unsafe source? The recorded analysis established that Release builds removed the assertion, the allocation had enough space, and ordinary safe fields could produce the layout.

A subtler objection concerned destruction. The compiler can use lean_dec_ref_known(..., 256) when it knows a constructor's layout. Direct destruction can therefore release the right number of fields despite the incorrect dynamic count. Looking only at that path could make the header truncation seem less consequential.

The ShareCommon copy changes the outcome. Its dynamic count causes it to omit the references that would keep the copied children alive. Later, static destruction releases the original references as expected. The copy and destruction routines disagree about ownership because they obtain the field count from different representations.

At 15:23 UTC, the judge recorded a real verdict with a confidence value of 0.99 and no unresolved assumptions. That was the agent's assessment of its source analysis. It was not a measurement of runtime behavior, and it did not replace reproduction.

Separating discovery from confirmation

The reporter re-read the relevant source and stored the affected function, dependencies, failed invariant, false-positive checks, patch guidance, and PoC plan. The resulting row was finding 73, “256-field constructors trigger use-after-free in ShareCommon.”

I then built the vulnerable revision, reproduced the crash, inspected the generated C, and filed the upstream report. The proof-forging variant was developed and tested after disclosure against the same underlying bug.

This sequence matters when describing what the system found. Winfunc identified the compiler/runtime mismatch and the safe-code ownership failure from source. Runtime execution confirmed the reported failure, and the later proof experiment demonstrated its effect on a native decision. Each result supports a different claim; the final theorem should not be presented as something the initial read-only scan executed.

For background on our earlier architecture, see How Asterisk Works. Other public results are covered in what our automated vulnerability research system has produced in practice.

The published reproducer

The complete Lake package pins nightly-2026-09-08, which contains the vulnerable runtime. It deliberately triggers a native use-after-free and should be run in a disposable environment.

unzip lean4-issue-15072-proof-forgery.zip
cd poc
lake test

The command builds the trigger as a native module, loads it during proof elaboration, checks the theorem, and runs a fail-closed executable. A successful run includes:

Built Main
'one_plus_one_eq_three' depends on axioms:
[propext, one_plus_one_eq_three._native.native_decide.ax_1_1]
native decision for 1 + 1 = 3: true

I also tested the package against the report's exact revision, 9bf5dc069a85c32fce20d074a628d85effff6e2a. With the compiler fix, the package is rejected before it can reach the runtime failure:

error: constructor 'Wide.mk' has too many fields

The fix

I filed issue #15072 at 16:47 UTC on September 8. Henrik Böving opened PR #15075 at 20:28 UTC, and it merged into master at 21:15 UTC that day as commit 9e3f6c6.

The corrected check enforces the runtime's exclusive limit:

if !c.size < maxCtorFields then
  throwCheckerError s!"constructor '{c.name}' has too many fields"

The patch also applies the exclusive check to the scalar-area limit and validates constructor layouts when they are computed, before they are cached. The IR checker retains the corresponding checks. This moves rejection earlier as well as correcting the comparison that admitted an unrepresentable count.

The added regression tests require errors for oversized object-field and scalar-field layouts. They check that the compiler rejects these declarations before the invalid layouts can reach the runtime.

Rejecting the layout is the appropriate primary fix because the runtime header cannot represent it. Fixing an individual consumer would leave other runtime code exposed to the same contradictory metadata. The compiler needs to enforce a layout that every consumer can interpret consistently.

A release-mode runtime check could provide additional protection if an invalid layout nevertheless reached the allocator. For this reported path, the compiler correction prevents safe source from producing the malformed constructor in the first place.

What the checked theorem means

Lean's proof-validation guidance treats validation as a question about the theorem statement, its assumptions, and the environment that checked it. The editor's check marks indicate that a proof was accepted relative to the declarations and axioms in that environment. They do not make every assumption true.

For this example, inspecting #print axioms exposes the native-evaluation dependency immediately. That is useful information for a reviewer. It makes the scope of the result explicit and allows a project to decide whether the additional assumption is acceptable.

There are good reasons to use native evaluation. A large computation may be impractical to carry out through ordinary reduction or explicit proof-term construction. PBLean, for example, describes both explicit proof construction and a reflection-based approach that executes a proved Boolean checker as native code. The paper explains the resulting dependence on compiler correctness alongside the scaling benefit.

The general distinction is between proving that a checking function is sound and trusting an implementation to execute that function faithfully. A proof about the function does not remove the need for that second assumption when its evaluation is delegated to native code. Our finding demonstrates a failure of that assumption; it does not establish that PBLean or another particular application was affected.

The validation requirements become stricter when the proof author may be adversarial. Lean's guidance recommends a theorem statement prepared in a trusted environment, a sandboxed build of the submitted proof, and checking through Comparator with external checkers. Those steps address different parts of the problem: what statement was actually proved, what code ran during the build, and which implementation checked the exported proof.

A proof that uses native evaluation still needs an explicit decision about its native assumptions. Rechecking the reasoning that follows from an axiom does not establish the truth of the axiom itself. The per-computation axiom design makes that dependency available for inspection rather than leaving it implicit in the acceptance result.

In this case, safe source was enough to reach an ownership failure in generated native code. The false arithmetic was the visible consequence of trusting the corrupted computation. A reviewer who inspects the theorem's assumptions can reject that result without confusing it with a failure of Lean's logic, and a fixed compiler rejects the malformed layout before the computation begins.