Skip to content
OpenAdvisories

Product · leanprover

lean4

2 known vulnerabilities.

lean4 at a glance

Last 12 months
2
Critical · all time
0
Exploited · all time
0
Public exploit · all time
2
New vulnerabilities per month · last 12 months
0 1 2 December 2025: 0 vulnerabilities Dec 2025 January 2026: 0 vulnerabilities February 2026: 0 vulnerabilities March 2026: 0 vulnerabilities Mar April 2026: 0 vulnerabilities May 2026: 0 vulnerabilities June 2026: 0 vulnerabilities Jun July 2026: 0 vulnerabilities August 2026: 2 vulnerabilities September 2026: 0 vulnerabilities Sep October 2026: 0 vulnerabilities November 2026: 0 vulnerabilities
Show as table
MonthVulnerabilitiesCritical
Nov 202600
Oct 202600
Sep 202600
Aug 202620
Jul 202600
Jun 202600
May 202600
Apr 202600
Mar 202600
Feb 202600
Jan 202600
Dec 202500
Nov 202500
Oct 202500
Sep 202500
Aug 202500
Jul 202500
Jun 202500
May 202500
Apr 202500
Mar 202500
Feb 202500
Jan 202500
Dec 202400
All Critical High Medium Low Exploited only Public exploit

2 results · Feed

  • Medium 6.3
    CVE-2026-72711 Public exploit

    Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

    The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the loc…

    leanprover lean4
  • Medium 6.3
    CVE-2026-72844 Public exploit

    Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

    The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are repla…

    leanprover lean4