CVE-2026-72711: Software Security Vulnerability Vulnerability

MODERATE
Advisory Identifier: GHSA-fhmq-xvc2-q54h
Share
CVSS 6.3
CWE-20
Published
Advisory Summary

CVE-2026-72711 is a MODERATE (CVSS 6.3) security vulnerability vulnerability (CWE-20: Improper Input Validation) affecting Software libraries in the Maven ecosystem. The weakness occurs when the product receives input or data, but it does not validate or incorrectly validates that the input has the properties that are required to process the data safely and correctly.. Remediation is available in the latest vendor maintenance releases.

CVE-2026-72711 at a Glance

CVE Identifier CVE-2026-72711
GHSA Identifier GHSA-fhmq-xvc2-q54h
Severity MODERATE
CVSS v3.1 Base Score 6.3
CWE Classification CWE-20: Improper Input Validation
Affected Product Software
Package Ecosystem Maven
Published Date
Last Updated

Security Impact

CVSS: 6.3

The security impact metrics below are parsed directly from the CVSS v3.1 vector string (CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N).

Attack Vector Local (AV:L)
Attack Complexity Low (AC:L)
Privileges Required None (PR:N)
User Interaction Required (UI:R)
Scope Changed (S:C)
Confidentiality None (C:N)
Integrity High (I:H)
Availability None (A:N)

How to Fix CVE-2026-72711

To remediate this vulnerability, upgrade all affected Software dependencies to a patched release. Both direct and transitive dependencies should be checked, as frameworks or security libraries may pull in vulnerable versions transitively.

Verify Direct and Transitive Dependencies

Run the following command in your project directory to verify that all resolved dependencies use the patched release: 

mvn dependency:tree

How to Check if You Are Affected

To determine whether your Java application is affected by CVE-2026-72711, inspect your build dependencies using the Maven Dependency Plugin:

mvn dependency:tree

Analyze the terminal output to locate any version of Software in your dependency tree. If any resolved version matches the vulnerable ranges listed in the table below (for example, versions earlier than the patched release), your application is affected.

Note: The mvn dependency:tree command inspects the resolved dependency graph declared in your project's POM files; it does not perform automated security scanning or inspect runtime dynamic classpaths. Always verify runtime container classpaths and shaded JARs.

Technical Details

Vulnerability Mechanism & Technical Analysis

This vulnerability is classified under CWE-20: Improper Input Validation, where the product receives input or data, but it does not validate or incorrectly validates that the input has the properties that are required to process the data safely and correctly. In Software, software state validation or input boundaries are circumvented during processing. Review the official source advisory statement below for specific affected components, classes, and reproduction details.

Source Advisory Statement

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 local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.

References

NVD — CVE-2026-72711 NVD
https://nvd.nist.gov/vuln/detail/CVE-2026-72711
Software Source Repository REPOSITORY
https://github.com/leanprover/lean4/issues/14484
Software Source Repository REPOSITORY
https://github.com/leanprover/lean4/pull/14498
Software Source Repository REPOSITORY
https://github.com/endrazine/lean-cve-poc-14484
Software Source Repository REPOSITORY
https://github.com/leanprover/lean4
www.vulncheck.com/advisories/lean-4-b... WEB
https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable

Frequently Asked Questions

What is CVE-2026-72711?
CVE-2026-72711 is a security vulnerability in Software classified as a security vulnerability vulnerability under CWE-20: Improper Input Validation.
Which Software versions are affected?
Affected versions include releases prior to current release patches.
What version fixes CVE-2026-72711?
Upgrading to current release patches (or the latest patched release for your respective branch) resolves the vulnerability.
What is the CVSS score of CVE-2026-72711?
CVE-2026-72711 has a CVSS v3.1 base score of 6.3 (MODERATE) with vector string CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N.
What CWE is associated with CVE-2026-72711?
CVE-2026-72711 is classified under CWE-20: Improper Input Validation (The product receives input or data, but it does not validate or incorrectly validates that the input has the properties that are required to process the data safely and correctly.).
How can I check Maven dependencies for CVE-2026-72711?
Run the dependency tree command: 'mvn dependency:tree'. This command lists direct and transitive dependencies in your build configuration so you can verify if a vulnerable version is resolved.
Machine-readable OSV JSON OSV v1.5 Schema
Normalized schema output
View Raw JSON 
{
  "schema_version" : "1.4.0",
  "id" : "GHSA-fhmq-xvc2-q54h",
  "modified" : "2026-08-24T21:33:44Z",
  "published" : "2026-08-24T21:33:44Z",
  "aliases" : [ "CVE-2026-72711" ],
  "details" : "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 local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.",
  "severity" : [ {
    "type" : "CVSS_V3",
    "score" : "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N"
  }, {
    "type" : "CVSS_V4",
    "score" : "CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X"
  } ],
  "affected" : [ ],
  "references" : [ {
    "type" : "ADVISORY",
    "url" : "https://nvd.nist.gov/vuln/detail/CVE-2026-72711"
  }, {
    "type" : "WEB",
    "url" : "https://github.com/leanprover/lean4/issues/14484"
  }, {
    "type" : "WEB",
    "url" : "https://github.com/leanprover/lean4/pull/14498"
  }, {
    "type" : "WEB",
    "url" : "https://github.com/endrazine/lean-cve-poc-14484"
  }, {
    "type" : "WEB",
    "url" : "https://github.com/leanprover/lean4"
  }, {
    "type" : "WEB",
    "url" : "https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable"
  } ],
  "database_specific" : {
    "cwe_ids" : [ "CWE-20" ],
    "severity" : "MODERATE",
    "github_reviewed" : false,
    "github_reviewed_at" : null,
    "nvd_published_at" : "2026-08-24T20:17:18Z"
  }
}