Skip to content
OpenAdvisories

Vendor

leanprover

3 known vulnerabilities.

Products

lean4 2 vscode-lean4 1
All Critical High Medium Low Exploited only Public exploit

2 results · Clear filters · 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