Search

Find a vulnerability

Search criteria ⓘ Use this form to refine search results.
Full-text search supports keyword queries with ranking and filtering.
You can combine vendor, product, and sources to narrow results.
Enable “Apply ordering” to sort by date instead of relevance.

    6 vulnerabilities by leanprover

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

    Vulnerability from nvd – Published: 2026-08-24 20:08 – Updated: 2026-08-24 20:14
    VLAI
    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
    References
    Impacted products
    Vendor Product Version
    leanprover lean4 Affected: 0 , < 4.32.2 (semver)
    		Create a notification for this product.
    Date Public
    2026-07-22 00:00
    Credits
    Patrick Hulin Jonathan Brossard (MOABI)
    Show details on NVD website
    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"
}

    CVE-2026-72844 (GCVE-0-2026-72844)

    Vulnerability from nvd – Published: 2026-08-20 17:19 – Updated: 2026-08-21 21:46
    VLAI
    Title
    Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
    Summary
    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 replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
    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
    SSVC
    Exploitation: poc Automatable: no Technical Impact: partial
    CISA Coordinator · CISA-ADP (v2.0.3)
    Decision recorded 2026-08-21 21:13 UTC
    CWE
    • CWE-843 - Access of Resource Using Incompatible Type ('Type Confusion')
    Assigner
    References
    Impacted products
    Vendor Product Version
    leanprover lean4 Affected: 0 , < 4.32.2 (semver)
    Unaffected: 4.32.2 (semver)
    Affected: 4.33.0-rc1 (semver)
    		Create a notification for this product.
    Date Public
    2026-07-28 00:00
    Credits
    kiranandcode Ramana Kumar (@xrchz) Leonardo de Moura Jonathan Brossard (MOABI)
    Show details on NVD website
    To clipboard 

    {
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-72844",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-21T21:13:48.944575Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-21T21:46:54.936Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "defaultStatus": "unaffected",
          "product": "lean4",
          "repo": "https://github.com/leanprover/lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "lessThan": "4.32.2",
              "status": "affected",
              "version": "0",
              "versionType": "semver"
            },
            {
              "status": "unaffected",
              "version": "4.32.2",
              "versionType": "semver"
            },
            {
              "status": "affected",
              "version": "4.33.0-rc1",
              "versionType": "semver"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "kiranandcode"
        },
        {
          "lang": "en",
          "type": "other",
          "value": "Ramana Kumar (@xrchz)"
        },
        {
          "lang": "en",
          "type": "remediation developer",
          "value": "Leonardo de Moura"
        },
        {
          "lang": "en",
          "type": "other",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2026-07-28T00:00:00.000Z",
      "descriptions": [
        {
          "lang": "en",
          "value": "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 replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency."
        }
      ],
      "metrics": [
        {
          "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"
        },
        {
          "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"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-843",
              "description": "Access of Resource Using Incompatible Type (\u0027Type Confusion\u0027)",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-08-21T11:20:58.955Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "name": "GitHub Issue #14576",
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/issues/14576"
        },
        {
          "name": "fix: missing check at kernel inductive declaration",
          "tags": [
            "patch"
          ],
          "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808"
        },
        {
          "name": "GitHub Pull Request #14577",
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/pull/14577"
        },
        {
          "name": "lean-cve-poc",
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/lean-cve-poc"
        },
        {
          "name": "CollatzLean",
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/xrchz/CollatzLean"
        },
        {
          "name": "oss-security: Lean 4 kernel soundness bug",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1"
        },
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/leanprover/lean4"
        },
        {
          "name": "VulnCheck Advisory: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections"
        }
      ],
      "timeline": [
        {
          "lang": "en",
          "time": "2026-07-25T00:00:00.000Z",
          "value": "CollatzLean repository published, exploiting the bug"
        },
        {
          "lang": "en",
          "time": "2026-07-28T00:00:00.000Z",
          "value": "Bug identified and reported in issue #14576"
        },
        {
          "lang": "en",
          "time": "2026-07-28T00:00:00.000Z",
          "value": "Fix submitted in pull request #14577"
        },
        {
          "lang": "en",
          "time": "2026-07-29T00:00:00.000Z",
          "value": "Fix available in nightly builds"
        },
        {
          "lang": "en",
          "time": "2026-08-02T00:00:00.000Z",
          "value": "Public advisory on oss-security"
        }
      ],
      "title": "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2026-72844",
    "datePublished": "2026-08-20T17:19:34.054Z",
    "dateReserved": "2026-08-10T15:14:51.467Z",
    "dateUpdated": "2026-08-21T21:46:54.936Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

    CVE-2026-32732 (GCVE-0-2026-32732)

    Vulnerability from nvd – Published: 2026-03-13 21:43 – Updated: 2026-03-16 20:22
    VLAI
    Title
    XSS in @leanprover/unicode-input-component
    Summary
    Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0.
    Severity
    0 (None)
    CVSS:4.0/AV:N/AC:L/AT:N/PR:N/UI:A/VC:N/VI:N/VA:N/SC:N/SI:N/SA:N
    SSVC
    Exploitation: none Automatable: no Technical Impact: partial
    CISA Coordinator · CISA-ADP (v2.0.3)
    Decision recorded 2026-03-16 20:09 UTC
    CWE
    • CWE-80 - Improper Neutralization of Script-Related HTML Tags in a Web Page (Basic XSS)
    Assigner
    References
    Impacted products
    Vendor Product Version
    leanprover vscode-lean4 Affected: < 0.2.0
    		Create a notification for this product.
    Show details on NVD website
    To clipboard 

    {
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-32732",
                "options": [
                  {
                    "Exploitation": "none"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-03-16T20:09:27.977368Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-03-16T20:22:43.428Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "product": "vscode-lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "status": "affected",
              "version": "\u003c 0.2.0"
            }
          ]
        }
      ],
      "descriptions": [
        {
          "lang": "en",
          "value": "Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0."
        }
      ],
      "metrics": [
        {
          "cvssV4_0": {
            "attackComplexity": "LOW",
            "attackRequirements": "NONE",
            "attackVector": "NETWORK",
            "baseScore": 0,
            "baseSeverity": "NONE",
            "privilegesRequired": "NONE",
            "subAvailabilityImpact": "NONE",
            "subConfidentialityImpact": "NONE",
            "subIntegrityImpact": "NONE",
            "userInteraction": "ACTIVE",
            "vectorString": "CVSS:4.0/AV:N/AC:L/AT:N/PR:N/UI:A/VC:N/VI:N/VA:N/SC:N/SI:N/SA:N",
            "version": "4.0",
            "vulnAvailabilityImpact": "NONE",
            "vulnConfidentialityImpact": "NONE",
            "vulnIntegrityImpact": "NONE"
          }
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-80",
              "description": "CWE-80: Improper Neutralization of Script-Related HTML Tags in a Web Page (Basic XSS)",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-03-13T21:43:22.209Z",
        "orgId": "a0819718-46f1-4df5-94e2-005712e83aaa",
        "shortName": "GitHub_M"
      },
      "references": [
        {
          "name": "https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r5h2",
          "tags": [
            "x_refsource_CONFIRM"
          ],
          "url": "https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r5h2"
        },
        {
          "name": "https://github.com/leanprover/vscode-lean4/pull/735",
          "tags": [
            "x_refsource_MISC"
          ],
          "url": "https://github.com/leanprover/vscode-lean4/pull/735"
        },
        {
          "name": "https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/near/578502003",
          "tags": [
            "x_refsource_MISC"
          ],
          "url": "https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/near/578502003"
        }
      ],
      "source": {
        "advisory": "GHSA-6ggm-pwr9-r5h2",
        "discovery": "UNKNOWN"
      },
      "title": "XSS in @leanprover/unicode-input-component"
    }
  },
  "cveMetadata": {
    "assignerOrgId": "a0819718-46f1-4df5-94e2-005712e83aaa",
    "assignerShortName": "GitHub_M",
    "cveId": "CVE-2026-32732",
    "datePublished": "2026-03-13T21:43:22.209Z",
    "dateReserved": "2026-03-13T15:02:00.627Z",
    "dateUpdated": "2026-03-16T20:22:43.428Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

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

    Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-08-24 20:14
    VLAI
    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
    References
    Impacted products
    Vendor Product Version
    leanprover lean4 Affected: 0 , < 4.32.2 (semver)
    		Create a notification for this product.
    Date Public
    2026-07-22 00:00
    Credits
    Patrick Hulin Jonathan Brossard (MOABI)
    Show details on NVD website
    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"
}

    CVE-2026-72844 (GCVE-0-2026-72844)

    Vulnerability from cvelistv5 – Published: 2026-08-20 17:19 – Updated: 2026-08-21 21:46
    VLAI
    Title
    Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
    Summary
    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 replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
    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
    SSVC
    Exploitation: poc Automatable: no Technical Impact: partial
    CISA Coordinator · CISA-ADP (v2.0.3)
    Decision recorded 2026-08-21 21:13 UTC
    CWE
    • CWE-843 - Access of Resource Using Incompatible Type ('Type Confusion')
    Assigner
    References
    Impacted products
    Vendor Product Version
    leanprover lean4 Affected: 0 , < 4.32.2 (semver)
    Unaffected: 4.32.2 (semver)
    Affected: 4.33.0-rc1 (semver)
    		Create a notification for this product.
    Date Public
    2026-07-28 00:00
    Credits
    kiranandcode Ramana Kumar (@xrchz) Leonardo de Moura Jonathan Brossard (MOABI)
    Show details on NVD website
    To clipboard 

    {
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-72844",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-21T21:13:48.944575Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-21T21:46:54.936Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "defaultStatus": "unaffected",
          "product": "lean4",
          "repo": "https://github.com/leanprover/lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "lessThan": "4.32.2",
              "status": "affected",
              "version": "0",
              "versionType": "semver"
            },
            {
              "status": "unaffected",
              "version": "4.32.2",
              "versionType": "semver"
            },
            {
              "status": "affected",
              "version": "4.33.0-rc1",
              "versionType": "semver"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "kiranandcode"
        },
        {
          "lang": "en",
          "type": "other",
          "value": "Ramana Kumar (@xrchz)"
        },
        {
          "lang": "en",
          "type": "remediation developer",
          "value": "Leonardo de Moura"
        },
        {
          "lang": "en",
          "type": "other",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2026-07-28T00:00:00.000Z",
      "descriptions": [
        {
          "lang": "en",
          "value": "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 replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency."
        }
      ],
      "metrics": [
        {
          "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"
        },
        {
          "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"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-843",
              "description": "Access of Resource Using Incompatible Type (\u0027Type Confusion\u0027)",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-08-21T11:20:58.955Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "name": "GitHub Issue #14576",
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/issues/14576"
        },
        {
          "name": "fix: missing check at kernel inductive declaration",
          "tags": [
            "patch"
          ],
          "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808"
        },
        {
          "name": "GitHub Pull Request #14577",
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/leanprover/lean4/pull/14577"
        },
        {
          "name": "lean-cve-poc",
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/lean-cve-poc"
        },
        {
          "name": "CollatzLean",
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/xrchz/CollatzLean"
        },
        {
          "name": "oss-security: Lean 4 kernel soundness bug",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1"
        },
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/leanprover/lean4"
        },
        {
          "name": "VulnCheck Advisory: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections"
        }
      ],
      "timeline": [
        {
          "lang": "en",
          "time": "2026-07-25T00:00:00.000Z",
          "value": "CollatzLean repository published, exploiting the bug"
        },
        {
          "lang": "en",
          "time": "2026-07-28T00:00:00.000Z",
          "value": "Bug identified and reported in issue #14576"
        },
        {
          "lang": "en",
          "time": "2026-07-28T00:00:00.000Z",
          "value": "Fix submitted in pull request #14577"
        },
        {
          "lang": "en",
          "time": "2026-07-29T00:00:00.000Z",
          "value": "Fix available in nightly builds"
        },
        {
          "lang": "en",
          "time": "2026-08-02T00:00:00.000Z",
          "value": "Public advisory on oss-security"
        }
      ],
      "title": "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2026-72844",
    "datePublished": "2026-08-20T17:19:34.054Z",
    "dateReserved": "2026-08-10T15:14:51.467Z",
    "dateUpdated": "2026-08-21T21:46:54.936Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

    CVE-2026-32732 (GCVE-0-2026-32732)

    Vulnerability from cvelistv5 – Published: 2026-03-13 21:43 – Updated: 2026-03-16 20:22
    VLAI
    Title
    XSS in @leanprover/unicode-input-component
    Summary
    Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0.
    Severity
    0 (None)
    CVSS:4.0/AV:N/AC:L/AT:N/PR:N/UI:A/VC:N/VI:N/VA:N/SC:N/SI:N/SA:N
    SSVC
    Exploitation: none Automatable: no Technical Impact: partial
    CISA Coordinator · CISA-ADP (v2.0.3)
    Decision recorded 2026-03-16 20:09 UTC
    CWE
    • CWE-80 - Improper Neutralization of Script-Related HTML Tags in a Web Page (Basic XSS)
    Assigner
    References
    Impacted products
    Vendor Product Version
    leanprover vscode-lean4 Affected: < 0.2.0
    		Create a notification for this product.
    Show details on NVD website
    To clipboard 

    {
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-32732",
                "options": [
                  {
                    "Exploitation": "none"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-03-16T20:09:27.977368Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-03-16T20:22:43.428Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "product": "vscode-lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "status": "affected",
              "version": "\u003c 0.2.0"
            }
          ]
        }
      ],
      "descriptions": [
        {
          "lang": "en",
          "value": "Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0."
        }
      ],
      "metrics": [
        {
          "cvssV4_0": {
            "attackComplexity": "LOW",
            "attackRequirements": "NONE",
            "attackVector": "NETWORK",
            "baseScore": 0,
            "baseSeverity": "NONE",
            "privilegesRequired": "NONE",
            "subAvailabilityImpact": "NONE",
            "subConfidentialityImpact": "NONE",
            "subIntegrityImpact": "NONE",
            "userInteraction": "ACTIVE",
            "vectorString": "CVSS:4.0/AV:N/AC:L/AT:N/PR:N/UI:A/VC:N/VI:N/VA:N/SC:N/SI:N/SA:N",
            "version": "4.0",
            "vulnAvailabilityImpact": "NONE",
            "vulnConfidentialityImpact": "NONE",
            "vulnIntegrityImpact": "NONE"
          }
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-80",
              "description": "CWE-80: Improper Neutralization of Script-Related HTML Tags in a Web Page (Basic XSS)",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-03-13T21:43:22.209Z",
        "orgId": "a0819718-46f1-4df5-94e2-005712e83aaa",
        "shortName": "GitHub_M"
      },
      "references": [
        {
          "name": "https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r5h2",
          "tags": [
            "x_refsource_CONFIRM"
          ],
          "url": "https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r5h2"
        },
        {
          "name": "https://github.com/leanprover/vscode-lean4/pull/735",
          "tags": [
            "x_refsource_MISC"
          ],
          "url": "https://github.com/leanprover/vscode-lean4/pull/735"
        },
        {
          "name": "https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/near/578502003",
          "tags": [
            "x_refsource_MISC"
          ],
          "url": "https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/near/578502003"
        }
      ],
      "source": {
        "advisory": "GHSA-6ggm-pwr9-r5h2",
        "discovery": "UNKNOWN"
      },
      "title": "XSS in @leanprover/unicode-input-component"
    }
  },
  "cveMetadata": {
    "assignerOrgId": "a0819718-46f1-4df5-94e2-005712e83aaa",
    "assignerShortName": "GitHub_M",
    "cveId": "CVE-2026-32732",
    "datePublished": "2026-03-13T21:43:22.209Z",
    "dateReserved": "2026-03-13T15:02:00.627Z",
    "dateUpdated": "2026-03-16T20:22:43.428Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}