Vulnerability-Lookup

CVE-2026-72711 (GCVE-0-2026-72711)

Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-08-24 20:14

Title

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

Summary

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

6.8 (Medium)


                        
                          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

6.3 (Medium)


                        
                          CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

SSVC

Exploitation: poc Automatable: no Technical Impact: partial

CISA Coordinator · CISA-ADP (v2.0.3)

Decision recorded 2026-08-24 20:14 UTC

CWE

CWE-20 - Improper Input Validation

Assigner

VulnCheck mitre root

References

5 references

URL	Tags
https://github.com/leanprover/lean4	product
https://github.com/leanprover/lean4/issues/14484	issue-tracking
https://github.com/leanprover/lean4/pull/14498	issue-tracking
https://github.com/endrazine/lean-cve-poc-14484	exploit
https://www.vulncheck.com/advisories/lean-4-befor…	third-party-advisory

Impacted products

1 product

Vendor	Product	Version	CPE status
leanprover	lean4	Affected: 0 , < 4.32.2 (semver)	guessed

Date Public

2026-07-22 00:00

Credits

Patrick Hulin Jonathan Brossard (MOABI)

Show details on NVD website

JSON

To clipboard

{
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-72711",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-24T20:14:31.474084Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-24T20:14:41.969Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "defaultStatus": "unaffected",
          "packageURL": "pkg:github/leanprover/lean4",
          "product": "lean4",
          "repo": "https://github.com/leanprover/lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "lessThan": "4.32.2",
              "status": "affected",
              "version": "0",
              "versionType": "semver"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Patrick Hulin"
        },
        {
          "lang": "en",
          "type": "reporter",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2026-07-22T00:00:00.000Z",
      "descriptions": [
        {
          "lang": "en",
          "value": "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\u0027s 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."
        }
      ],
      "metrics": [
        {
          "cvssV4_0": {
            "attackComplexity": "LOW",
            "attackRequirements": "NONE",
            "attackVector": "LOCAL",
            "baseScore": 6.8,
            "baseSeverity": "MEDIUM",
            "privilegesRequired": "NONE",
            "subAvailabilityImpact": "NONE",
            "subConfidentialityImpact": "NONE",
            "subIntegrityImpact": "NONE",
            "userInteraction": "PASSIVE",
            "vectorString": "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",
            "version": "4.0",
            "vulnAvailabilityImpact": "NONE",
            "vulnConfidentialityImpact": "NONE",
            "vulnIntegrityImpact": "HIGH"
          },
          "format": "CVSS"
        },
        {
          "cvssV3_1": {
            "attackComplexity": "LOW",
            "attackVector": "LOCAL",
            "availabilityImpact": "NONE",
            "baseScore": 6.3,
            "baseSeverity": "MEDIUM",
            "confidentialityImpact": "NONE",
            "integrityImpact": "HIGH",
            "privilegesRequired": "NONE",
            "scope": "CHANGED",
            "userInteraction": "REQUIRED",
            "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
            "version": "3.1"
          },
          "format": "CVSS"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-20",
              "description": "Improper Input Validation",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-08-24T20:08:33.219Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/leanprover/lean4"
        },
        {
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/issues/14484"
        },
        {
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/pull/14498"
        },
        {
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/lean-cve-poc-14484"
        },
        {
          "name": "VulnCheck Advisory: Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable"
        }
      ],
      "title": "Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2026-72711",
    "datePublished": "2026-08-24T20:08:33.219Z",
    "dateReserved": "2026-08-10T13:02:52.001Z",
    "dateUpdated": "2026-08-24T20:14:41.969Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2",
  "vulnerability-lookup:meta": {
    "epss": {
      "cve": "CVE-2026-72711",
      "date": "2026-08-25",
      "epss": "0.0012",
      "percentile": "0.02035"
    },
    "nvd": "{\"cve\":{\"id\":\"CVE-2026-72711\",\"sourceIdentifier\":\"disclosure@vulncheck.com\",\"published\":\"2026-08-24T20:17:18.657\",\"lastModified\":\"2026-08-24T21:17:46.790\",\"vulnStatus\":\"Received\",\"cveTags\":[],\"descriptions\":[{\"lang\":\"en\",\"value\":\"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\u0027s 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.\"}],\"affected\":[{\"source\":\"disclosure@vulncheck.com\",\"affectedData\":[{\"vendor\":\"leanprover\",\"product\":\"lean4\",\"defaultStatus\":\"unaffected\",\"repo\":\"https://github.com/leanprover/lean4\",\"packageURL\":\"pkg:github/leanprover/lean4\",\"versions\":[{\"version\":\"0\",\"lessThan\":\"4.32.2\",\"versionType\":\"semver\",\"status\":\"affected\"}]}]}],\"metrics\":{\"cvssMetricV40\":[{\"source\":\"disclosure@vulncheck.com\",\"type\":\"Secondary\",\"cvssData\":{\"version\":\"4.0\",\"vectorString\":\"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\",\"baseScore\":6.8,\"baseSeverity\":\"MEDIUM\",\"attackVector\":\"LOCAL\",\"attackComplexity\":\"LOW\",\"attackRequirements\":\"NONE\",\"privilegesRequired\":\"NONE\",\"userInteraction\":\"PASSIVE\",\"vulnConfidentialityImpact\":\"NONE\",\"vulnIntegrityImpact\":\"HIGH\",\"vulnAvailabilityImpact\":\"NONE\",\"subConfidentialityImpact\":\"NONE\",\"subIntegrityImpact\":\"NONE\",\"subAvailabilityImpact\":\"NONE\",\"exploitMaturity\":\"NOT_DEFINED\",\"confidentialityRequirement\":\"NOT_DEFINED\",\"integrityRequirement\":\"NOT_DEFINED\",\"availabilityRequirement\":\"NOT_DEFINED\",\"modifiedAttackVector\":\"NOT_DEFINED\",\"modifiedAttackComplexity\":\"NOT_DEFINED\",\"modifiedAttackRequirements\":\"NOT_DEFINED\",\"modifiedPrivilegesRequired\":\"NOT_DEFINED\",\"modifiedUserInteraction\":\"NOT_DEFINED\",\"modifiedVulnConfidentialityImpact\":\"NOT_DEFINED\",\"modifiedVulnIntegrityImpact\":\"NOT_DEFINED\",\"modifiedVulnAvailabilityImpact\":\"NOT_DEFINED\",\"modifiedSubConfidentialityImpact\":\"NOT_DEFINED\",\"modifiedSubIntegrityImpact\":\"NOT_DEFINED\",\"modifiedSubAvailabilityImpact\":\"NOT_DEFINED\",\"Safety\":\"NOT_DEFINED\",\"Automatable\":\"NOT_DEFINED\",\"Recovery\":\"NOT_DEFINED\",\"valueDensity\":\"NOT_DEFINED\",\"vulnerabilityResponseEffort\":\"NOT_DEFINED\",\"providerUrgency\":\"NOT_DEFINED\"}}],\"cvssMetricV31\":[{\"source\":\"disclosure@vulncheck.com\",\"type\":\"Secondary\",\"cvssData\":{\"version\":\"3.1\",\"vectorString\":\"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N\",\"baseScore\":6.3,\"baseSeverity\":\"MEDIUM\",\"attackVector\":\"LOCAL\",\"attackComplexity\":\"LOW\",\"privilegesRequired\":\"NONE\",\"userInteraction\":\"REQUIRED\",\"scope\":\"CHANGED\",\"confidentialityImpact\":\"NONE\",\"integrityImpact\":\"HIGH\",\"availabilityImpact\":\"NONE\"},\"exploitabilityScore\":1.8,\"impactScore\":4.0}],\"ssvcV203\":[{\"source\":\"134c704f-9b21-4f2e-91b3-4a467353bcc0\",\"ssvcData\":{\"timestamp\":\"2026-08-24T20:14:31.474084Z\",\"id\":\"CVE-2026-72711\",\"options\":[{\"exploitation\":\"poc\"},{\"automatable\":\"no\"},{\"technicalImpact\":\"partial\"}],\"role\":\"CISA Coordinator\",\"version\":\"2.0.3\"}}]},\"weaknesses\":[{\"source\":\"disclosure@vulncheck.com\",\"type\":\"Secondary\",\"description\":[{\"lang\":\"en\",\"value\":\"CWE-20\"}]}],\"references\":[{\"url\":\"https://github.com/endrazine/lean-cve-poc-14484\",\"source\":\"disclosure@vulncheck.com\"},{\"url\":\"https://github.com/leanprover/lean4\",\"source\":\"disclosure@vulncheck.com\"},{\"url\":\"https://github.com/leanprover/lean4/issues/14484\",\"source\":\"disclosure@vulncheck.com\"},{\"url\":\"https://github.com/leanprover/lean4/pull/14498\",\"source\":\"disclosure@vulncheck.com\"},{\"url\":\"https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable\",\"source\":\"disclosure@vulncheck.com\"}]}}",
    "vulnrichment": {
      "containers": "{\"adp\": [{\"title\": \"CISA ADP Vulnrichment\", \"metrics\": [{\"other\": {\"type\": \"ssvc\", \"content\": {\"id\": \"CVE-2026-72711\", \"role\": \"CISA Coordinator\", \"options\": [{\"Exploitation\": \"poc\"}, {\"Automatable\": \"no\"}, {\"Technical Impact\": \"partial\"}], \"version\": \"2.0.3\", \"timestamp\": \"2026-08-24T20:14:31.474084Z\"}}}], \"providerMetadata\": {\"orgId\": \"134c704f-9b21-4f2e-91b3-4a467353bcc0\", \"shortName\": \"CISA-ADP\", \"dateUpdated\": \"2026-08-24T20:14:38.025Z\"}}], \"cna\": {\"title\": \"Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable\", \"credits\": [{\"lang\": \"en\", \"type\": \"finder\", \"value\": \"Patrick Hulin\"}, {\"lang\": \"en\", \"type\": \"reporter\", \"value\": \"Jonathan Brossard (MOABI)\"}], \"metrics\": [{\"format\": \"CVSS\", \"cvssV4_0\": {\"version\": \"4.0\", \"baseScore\": 6.8, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"vectorString\": \"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\", \"userInteraction\": \"PASSIVE\", \"attackComplexity\": \"LOW\", \"attackRequirements\": \"NONE\", \"privilegesRequired\": \"NONE\", \"subIntegrityImpact\": \"NONE\", \"vulnIntegrityImpact\": \"HIGH\", \"subAvailabilityImpact\": \"NONE\", \"vulnAvailabilityImpact\": \"NONE\", \"subConfidentialityImpact\": \"NONE\", \"vulnConfidentialityImpact\": \"NONE\"}}, {\"format\": \"CVSS\", \"cvssV3_1\": {\"scope\": \"CHANGED\", \"version\": \"3.1\", \"baseScore\": 6.3, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"vectorString\": \"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N\", \"integrityImpact\": \"HIGH\", \"userInteraction\": \"REQUIRED\", \"attackComplexity\": \"LOW\", \"availabilityImpact\": \"NONE\", \"privilegesRequired\": \"NONE\", \"confidentialityImpact\": \"NONE\"}}], \"affected\": [{\"repo\": \"https://github.com/leanprover/lean4\", \"vendor\": \"leanprover\", \"product\": \"lean4\", \"versions\": [{\"status\": \"affected\", \"version\": \"0\", \"lessThan\": \"4.32.2\", \"versionType\": \"semver\"}], \"packageURL\": \"pkg:github/leanprover/lean4\", \"defaultStatus\": \"unaffected\"}], \"datePublic\": \"2026-07-22T00:00:00.000Z\", \"references\": [{\"url\": \"https://github.com/leanprover/lean4\", \"tags\": [\"product\"]}, {\"url\": \"https://github.com/leanprover/lean4/issues/14484\", \"tags\": [\"issue-tracking\"]}, {\"url\": \"https://github.com/leanprover/lean4/pull/14498\", \"tags\": [\"issue-tracking\"]}, {\"url\": \"https://github.com/endrazine/lean-cve-poc-14484\", \"tags\": [\"exploit\"]}, {\"url\": \"https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable\", \"name\": \"VulnCheck Advisory: Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable\", \"tags\": [\"third-party-advisory\"]}], \"x_generator\": {\"engine\": \"vulncheck-endgame\"}, \"descriptions\": [{\"lang\": \"en\", \"value\": \"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\u0027s 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.\"}], \"problemTypes\": [{\"descriptions\": [{\"lang\": \"en\", \"type\": \"CWE\", \"cweId\": \"CWE-20\", \"description\": \"Improper Input Validation\"}]}], \"providerMetadata\": {\"orgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"shortName\": \"VulnCheck\", \"dateUpdated\": \"2026-08-24T20:08:33.219Z\"}}}",
      "cveMetadata": "{\"cveId\": \"CVE-2026-72711\", \"state\": \"PUBLISHED\", \"dateUpdated\": \"2026-08-24T20:14:41.969Z\", \"dateReserved\": \"2026-08-10T13:02:52.001Z\", \"assignerOrgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"datePublished\": \"2026-08-24T20:08:33.219Z\", \"assignerShortName\": \"VulnCheck\"}",
      "dataType": "CVE_RECORD",
      "dataVersion": "5.2"
    }
  }
}

FKIE_CVE-2026-72711

Vulnerability from fkie_nvd - Published: 2026-08-24 20:17 - Updated: 2026-08-24 21:17

Severity

6.3 (Medium) - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

Summary

References

	URL	Tags
	disclosure@vulncheck.com	https://github.com/endrazine/lean-cve-poc-14484
	disclosure@vulncheck.com	https://github.com/leanprover/lean4
	disclosure@vulncheck.com	https://github.com/leanprover/lean4/issues/14484
	disclosure@vulncheck.com	https://github.com/leanprover/lean4/pull/14498
	disclosure@vulncheck.com	https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable

Impacted products

	Vendor	Product	Version

JSON

To clipboard

{
  "affected": [
    {
      "affectedData": [
        {
          "defaultStatus": "unaffected",
          "packageURL": "pkg:github/leanprover/lean4",
          "product": "lean4",
          "repo": "https://github.com/leanprover/lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "lessThan": "4.32.2",
              "status": "affected",
              "version": "0",
              "versionType": "semver"
            }
          ]
        }
      ],
      "source": "disclosure@vulncheck.com"
    }
  ],
  "cveTags": [],
  "descriptions": [
    {
      "lang": "en",
      "value": "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\u0027s 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."
    }
  ],
  "id": "CVE-2026-72711",
  "lastModified": "2026-08-24T21:17:46.790",
  "metrics": {
    "cvssMetricV31": [
      {
        "cvssData": {
          "attackComplexity": "LOW",
          "attackVector": "LOCAL",
          "availabilityImpact": "NONE",
          "baseScore": 6.3,
          "baseSeverity": "MEDIUM",
          "confidentialityImpact": "NONE",
          "integrityImpact": "HIGH",
          "privilegesRequired": "NONE",
          "scope": "CHANGED",
          "userInteraction": "REQUIRED",
          "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
          "version": "3.1"
        },
        "exploitabilityScore": 1.8,
        "impactScore": 4.0,
        "source": "disclosure@vulncheck.com",
        "type": "Secondary"
      }
    ],
    "cvssMetricV40": [
      {
        "cvssData": {
          "Automatable": "NOT_DEFINED",
          "Recovery": "NOT_DEFINED",
          "Safety": "NOT_DEFINED",
          "attackComplexity": "LOW",
          "attackRequirements": "NONE",
          "attackVector": "LOCAL",
          "availabilityRequirement": "NOT_DEFINED",
          "baseScore": 6.8,
          "baseSeverity": "MEDIUM",
          "confidentialityRequirement": "NOT_DEFINED",
          "exploitMaturity": "NOT_DEFINED",
          "integrityRequirement": "NOT_DEFINED",
          "modifiedAttackComplexity": "NOT_DEFINED",
          "modifiedAttackRequirements": "NOT_DEFINED",
          "modifiedAttackVector": "NOT_DEFINED",
          "modifiedPrivilegesRequired": "NOT_DEFINED",
          "modifiedSubAvailabilityImpact": "NOT_DEFINED",
          "modifiedSubConfidentialityImpact": "NOT_DEFINED",
          "modifiedSubIntegrityImpact": "NOT_DEFINED",
          "modifiedUserInteraction": "NOT_DEFINED",
          "modifiedVulnAvailabilityImpact": "NOT_DEFINED",
          "modifiedVulnConfidentialityImpact": "NOT_DEFINED",
          "modifiedVulnIntegrityImpact": "NOT_DEFINED",
          "privilegesRequired": "NONE",
          "providerUrgency": "NOT_DEFINED",
          "subAvailabilityImpact": "NONE",
          "subConfidentialityImpact": "NONE",
          "subIntegrityImpact": "NONE",
          "userInteraction": "PASSIVE",
          "valueDensity": "NOT_DEFINED",
          "vectorString": "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",
          "version": "4.0",
          "vulnAvailabilityImpact": "NONE",
          "vulnConfidentialityImpact": "NONE",
          "vulnIntegrityImpact": "HIGH",
          "vulnerabilityResponseEffort": "NOT_DEFINED"
        },
        "source": "disclosure@vulncheck.com",
        "type": "Secondary"
      }
    ],
    "ssvcV203": [
      {
        "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
        "ssvcData": {
          "id": "CVE-2026-72711",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "partial"
            }
          ],
          "role": "CISA Coordinator",
          "timestamp": "2026-08-24T20:14:31.474084Z",
          "version": "2.0.3"
        }
      }
    ]
  },
  "published": "2026-08-24T20:17:18.657",
  "references": [
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/endrazine/lean-cve-poc-14484"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4/issues/14484"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4/pull/14498"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable"
    }
  ],
  "sourceIdentifier": "disclosure@vulncheck.com",
  "vulnStatus": "Received",
  "weaknesses": [
    {
      "description": [
        {
          "lang": "en",
          "value": "CWE-20"
        }
      ],
      "source": "disclosure@vulncheck.com",
      "type": "Secondary"
    }
  ]
}

GHSA-FHMQ-XVC2-Q54H

Vulnerability from github – Published: 2026-08-24 21:33 – Updated: 2026-08-24 21:33

Details

Severity

6.3 (Medium)


                  
                    CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

6.8 (Medium)


                  
                    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

Show details on source website

JSON

To clipboard

{
  "affected": [],
  "aliases": [
    "CVE-2026-72711"
  ],
  "database_specific": {
    "cwe_ids": [
      "CWE-20"
    ],
    "github_reviewed": false,
    "github_reviewed_at": null,
    "nvd_published_at": "2026-08-24T20:17:18Z",
    "severity": "MODERATE"
  },
  "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\u0027s 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.",
  "id": "GHSA-fhmq-xvc2-q54h",
  "modified": "2026-08-24T21:33:44Z",
  "published": "2026-08-24T21:33:44Z",
  "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"
    }
  ],
  "schema_version": "1.4.0",
  "severity": [
    {
      "score": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
      "type": "CVSS_V3"
    },
    {
      "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",
      "type": "CVSS_V4"
    }
  ]
}

Sightings

Author	Source	Type	Date	Other

Nomenclature

Seen: The vulnerability was mentioned, discussed, or observed by the user.
Confirmed: The vulnerability has been validated from an analyst's perspective.
Published Proof of Concept: A public proof of concept is available for this vulnerability.
Exploited: The vulnerability was observed as exploited by the user who reported the sighting.
Patched: The vulnerability was observed as successfully patched by the user who reported the sighting.
Not exploited: The vulnerability was not observed as exploited by the user who reported the sighting.
Not confirmed: The user expressed doubt about the validity of the vulnerability.
Not patched: The vulnerability was not observed as successfully patched by the user who reported the sighting.

Detection rules are retrieved from Rulezet.

The MITRE ATT&CK techniques below are AI-generated suggestions, inferred from the description of the vulnerability by the CIRCL/vulnerability-attack-technique-classification-roberta-base model, served locally by ML-Gateway. They have not been verified by an analyst and are provided for guidance only.
The approach is described in our paper Mapping CVEs to MITRE ATT&CK Techniques: A Curated Gold-Set Classifier and the Limits of LLM-Assisted Label Expansion.

Action not permitted

CVE-2026-72711 (GCVE-0-2026-72711)

FKIE_CVE-2026-72711

GHSA-FHMQ-XVC2-Q54H

Tags

Sightings

Nomenclature