Vulnerability-Lookup

Search criteria

Vendor

Product

Assigner (CNA or root)

Sources

Sort by

Order

CVSS min

CVSS max

Apply ordering (override relevance)

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

Vulnerability from nvd – Published: 2026-08-20 17:19 – Updated: 2026-08-21 21:46

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

VulnCheck mitre root

References

8 references

URL	Tags
https://github.com/leanprover/lean4/issues/14576	issue-tracking
https://github.com/leanprover/lean4/commit/a39eab…	patch
https://github.com/leanprover/lean4/pull/14577	issue-tracking
https://github.com/endrazine/lean-cve-poc	exploit
https://github.com/xrchz/CollatzLean	exploit
https://www.openwall.com/lists/oss-security/2026/…	third-party-advisory
https://github.com/leanprover/lean4	product
https://www.vulncheck.com/advisories/lean-4-kerne…	third-party-advisory

Impacted products

1 product

Vendor	Product	Version
leanprover	lean4	Affected: 0 , < 4.32.2 (semver) Unaffected: 4.32.2 (semver) Affected: 4.33.0-rc1 (semver)

Date Public

2026-07-28 00:00

Credits

kiranandcode Ramana Kumar (@xrchz) Leonardo de Moura Jonathan Brossard (MOABI)

Show details on NVD website

JSON

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

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)