Skip to content
NewA calmer, faster ZeroHour
StoryVulnerabilitymedium

Two Lean 4 kernel bugs accept checked proofs of False

1 source · 2 articlesFirst reported Updated ()2
What's new

First merged summary.

Merged summary · x-ai/grok-4.7 · rewritten as coverage arrivesSummaries by Vani AI

Jonathan Brossard disclosed two Lean 4 kernel soundness bugs that accept proofs of False, including 0 = 1, with no fixes stated.

Jonathan Brossard reported two Lean 4 kernel soundness bugs to oss-security on October 25. CVE-2026-72844 lets a projection name a structure that does not match the projected value; environment::add_inductive in src/kernel/inductive.cpp also did not type-check nested inductives, according to the truncated post. CVE-2026-72711 lets add_opaque skip the check_no_metavar_no_fvar closure check used on definition and theorem paths, described as inference cache poisoning; the snippet cuts off before the full mechanism. Both accept a proof of False, including 0 = 1, without axioms, sorry, unsafeCast, or modified .olean files; the second also passes at --trust=0 without debug.skipKernelTC. Neither post states an affected or fixed Lean version.

Key facts
  • CVE-2026-72844: projection structure names are not checked against value types.
  • add_inductive in src/kernel/inductive.cpp did not type-check nested inductives.
  • CVE-2026-72711: add_opaque omits check_no_metavar_no_fvar.
  • The second bug is accepted at --trust=0.
  • No affected or fixed Lean version is stated.
Analyze CVE-2026-72711 with Vani AIImpact, affected versions, exploitation, mitigations and detection

Timeline

dated events in the reporting · oldest first
  1. Oct 25, 2026Brossard posts two Lean 4 kernel soundness bugs. · oss-security

What each outlet adds

beyond the shared facts
  • oss-securityCVE-2026-72844: mismatched projection structures and unchecked nested inductives.
  • oss-securityCVE-2026-72711: add_opaque skips the closure check at --trust=0.
CVEs
CVE-2026-72711CVE-2026-72844
Products
Lean 4

Coverage

oldest first · one row per article · UTC
  1. · 5d ago oss-securityFirst report

    Lean 4 kernel forges proofs via nested projections (CVE-2026-72844)

    A projection can name a structure that does not match the projected value, yielding a checked proof of False.

  2. · 5d ago oss-security

    Lean 4 kernel accepts false proofs via opaque declarations (CVE-2026-72711)

    A checked proof of False, including 0 = 1, passes the Lean 4 kernel at --trust=0 without axioms or unsafe features.

Vulnerabilities in this story

All
CVEVulnerabilityCVSSEPSSSignalsPublished
CVE-2026-72711
The Lean 4 kernel does not check that the body of an opaque declaration is closed
6.8<1%
CVE-2026-72844
The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and…
6.8<1%