Vulnerability-Lookup

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

Vulnerability from cvelistv5 – Published: 2026-08-20 17:19 – Updated: 2026-11-08 14:08

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 CNA under the mitre root

CNA scorecard B 84/100 over 7808 records in the last 180 days details

References

9 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-trackingpatch
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
http://www.openwall.com/lists/oss-security/2026/10/26/2

Impacted products

1 product

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

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"
      },
      {
        "providerMetadata": {
          "dateUpdated": "2026-10-26T01:23:59.293Z",
          "orgId": "af854a3a-2127-422b-91ae-364da2661108",
          "shortName": "CVE"
        },
        "references": [
          {
            "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"
          }
        ],
        "title": "CVE Program Container"
      }
    ],
    "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-11-08T14:08:40.851Z",
        "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",
            "patch"
          ],
          "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-11-08T14:08:40.851Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2",
  "vulnerability-lookup:meta": {
    "epss": {
      "cve": "CVE-2026-72844",
      "date": "2026-11-10",
      "epss": "0.00187",
      "percentile": "0.08328"
    },
    "nvd": {
      "cve": {
        "affected": [
          {
            "affectedData": [
              {
                "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"
                  }
                ]
              }
            ],
            "source": "disclosure@vulncheck.com"
          }
        ],
        "cveTags": [],
        "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."
          },
          {
            "lang": "es",
            "value": "El kernel de Lean 4 no verifica que la estructura nombrada en una expresi\u00f3n de proyecci\u00f3n coincida con el tipo del valor que se est\u00e1 proyectando, y environment::add_inductive en src/kernel/inductive.cpp no comprob\u00f3 el tipo de las aplicaciones inductivas anidadas que son reemplazadas por tipos auxiliares, por lo que sus argumentos param\u00e9tricos escaparon a la verificaci\u00f3n. Un metaprograma ejecut\u00e1ndose en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyecci\u00f3n .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaraci\u00f3n a trav\u00e9s de la ruta addDecl comprobada ordinaria con la m\u00e1xima verificaci\u00f3n del kernel, sin sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, o un archivo .olean modificado. El resultado es una confusi\u00f3n de tipos que produce una prueba de Falso que no conlleva axiomas, de la cual se puede derivar cualquier proposici\u00f3n. La prueba de concepto publicada adem\u00e1s rellena dos expresiones hasta que sus hashes y profundidades aproximadas colisionan, lo que anula el almacenamiento en cach\u00e9 del kernel; esa es la t\u00e9cnica utilizada para alcanzar la falla, no su causa. La explotaci\u00f3n requiere ejecutar un metaprograma en proceso, por ejemplo, construyendo un proyecto o importando una dependencia maliciosa de Lake."
          }
        ],
        "id": "CVE-2026-72844",
        "lastModified": "2026-10-26T02:17:07.847",
        "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-72844",
                "options": [
                  {
                    "exploitation": "poc"
                  },
                  {
                    "automatable": "no"
                  },
                  {
                    "technicalImpact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-21T21:13:48.944575Z",
                "version": "2.0.3"
              }
            }
          ]
        },
        "published": "2026-08-20T18:16:45.290",
        "references": [
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/endrazine/lean-cve-poc"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/leanprover/lean4"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/leanprover/lean4/issues/14576"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/leanprover/lean4/pull/14577"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://github.com/xrchz/CollatzLean"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1"
          },
          {
            "source": "disclosure@vulncheck.com",
            "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections"
          },
          {
            "source": "af854a3a-2127-422b-91ae-364da2661108",
            "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"
          }
        ],
        "sourceIdentifier": "disclosure@vulncheck.com",
        "vulnStatus": "Deferred",
        "weaknesses": [
          {
            "description": [
              {
                "lang": "en",
                "value": "CWE-843"
              }
            ],
            "source": "disclosure@vulncheck.com",
            "type": "Secondary"
          }
        ]
      }
    },
    "vulnrichment": {
      "containers": {
        "adp": [
          {
            "providerMetadata": {
              "dateUpdated": "2026-10-26T01:23:59.293Z",
              "orgId": "af854a3a-2127-422b-91ae-364da2661108",
              "shortName": "CVE"
            },
            "references": [
              {
                "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"
              }
            ],
            "title": "CVE Program Container"
          },
          {
            "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:13:57.269Z",
              "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-11-08T14:08:40.851Z",
            "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",
                "patch"
              ],
              "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-11-08T14:08:40.851Z",
        "state": "PUBLISHED"
      },
      "dataType": "CVE_RECORD",
      "dataVersion": "5.2"
    }
  }
}

FKIE_CVE-2026-72844

Vulnerability from fkie_nvd - Published: 2026-08-20 18:16 - Updated: 2026-10-26 02: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
	disclosure@vulncheck.com	https://github.com/leanprover/lean4
	disclosure@vulncheck.com	https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808
	disclosure@vulncheck.com	https://github.com/leanprover/lean4/issues/14576
	disclosure@vulncheck.com	https://github.com/leanprover/lean4/pull/14577
	disclosure@vulncheck.com	https://github.com/xrchz/CollatzLean
	disclosure@vulncheck.com	https://www.openwall.com/lists/oss-security/2026/08/02/1
	disclosure@vulncheck.com	https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections
	af854a3a-2127-422b-91ae-364da2661108	http://www.openwall.com/lists/oss-security/2026/10/26/2

Impacted products

	Vendor	Product	Version

JSON

To clipboard

{
  "affected": [
    {
      "affectedData": [
        {
          "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"
            }
          ]
        }
      ],
      "source": "disclosure@vulncheck.com"
    }
  ],
  "cveTags": [],
  "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."
    },
    {
      "lang": "es",
      "value": "El kernel de Lean 4 no verifica que la estructura nombrada en una expresi\u00f3n de proyecci\u00f3n coincida con el tipo del valor que se est\u00e1 proyectando, y environment::add_inductive en src/kernel/inductive.cpp no comprob\u00f3 el tipo de las aplicaciones inductivas anidadas que son reemplazadas por tipos auxiliares, por lo que sus argumentos param\u00e9tricos escaparon a la verificaci\u00f3n. Un metaprograma ejecut\u00e1ndose en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyecci\u00f3n .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaraci\u00f3n a trav\u00e9s de la ruta addDecl comprobada ordinaria con la m\u00e1xima verificaci\u00f3n del kernel, sin sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, o un archivo .olean modificado. El resultado es una confusi\u00f3n de tipos que produce una prueba de Falso que no conlleva axiomas, de la cual se puede derivar cualquier proposici\u00f3n. La prueba de concepto publicada adem\u00e1s rellena dos expresiones hasta que sus hashes y profundidades aproximadas colisionan, lo que anula el almacenamiento en cach\u00e9 del kernel; esa es la t\u00e9cnica utilizada para alcanzar la falla, no su causa. La explotaci\u00f3n requiere ejecutar un metaprograma en proceso, por ejemplo, construyendo un proyecto o importando una dependencia maliciosa de Lake."
    }
  ],
  "id": "CVE-2026-72844",
  "lastModified": "2026-10-26T02:17:07.847",
  "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-72844",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "partial"
            }
          ],
          "role": "CISA Coordinator",
          "timestamp": "2026-08-21T21:13:48.944575Z",
          "version": "2.0.3"
        }
      }
    ]
  },
  "published": "2026-08-20T18:16:45.290",
  "references": [
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/endrazine/lean-cve-poc"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4/issues/14576"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/leanprover/lean4/pull/14577"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://github.com/xrchz/CollatzLean"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1"
    },
    {
      "source": "disclosure@vulncheck.com",
      "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections"
    },
    {
      "source": "af854a3a-2127-422b-91ae-364da2661108",
      "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"
    }
  ],
  "sourceIdentifier": "disclosure@vulncheck.com",
  "vulnStatus": "Deferred",
  "weaknesses": [
    {
      "description": [
        {
          "lang": "en",
          "value": "CWE-843"
        }
      ],
      "source": "disclosure@vulncheck.com",
      "type": "Secondary"
    }
  ]
}

GCVE-1988-2026-0441

Vulnerability from gna-1988 – Published: 2026-11-02 07:29 – Updated: 2026-11-02 07:29

Title

[Bugtraq] CVE-2026-72844: Lean 4 kernel soundness bug — forging proofs via nested inductive projections (0 = 1 demonstrated)

Summary

1. Summary ========== A soundness bug in the Lean 4 kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, sorry, unsafeCast, or modified .olean files. The kernel does not verify that the structure named in a projection expression matches the type of the value being projected. Additionally, environment::add_inductive in src/kernel/inductive.cpp did not type-check nested inductive applications, leaving their parameters unchecked. A metaprogram can register an ill-typed nested inductive and produce a proof of False at maximum kernel checking (--trust=0). The proof of concept pads expressions to force hash collisions, defeating kernel caching. This is the means of reaching the flaw, not its cause. 2. Context ========== Lean 4 is increasingly used as a foundation for formally verified software, proof-carrying code, and mathematical libraries. Its kernel is the trusted core: every theorem must pass kernel type-checking before it is accepted. A soundness bug in the kernel undermines the guarantees of any system built on top of it. Formally verified systems certified under Common Criteria (ISO 15408) or DO-178C (airborne software) derive their assurance from the correctness of the proof checker. A kernel-level bypass invalidates that assurance chain. Independent checkers such as Nanoda and lean4lean replay proofs against the same kernel rules and are therefore equally affected. 3. Impact ========= - Formally verified software: any proposition can be "proved" and kernel-checked, including safety properties of compilers, OS kernels, and cryptographic libraries. - Proof-carrying code: a malicious Lake dependency could inject unsound declarations that pass kernel checking. - Mathematical proof verification: results checked by the Lean kernel cannot be trusted on affected versions. 4. Proof of Concept =================== A Docker-reproducible PoC is available: git clone https://github.com/endrazine/lean-cve-poc cd lean-cve-poc docker build -t lean-cve-poc . docker run --rm lean-cve-poc On a vulnerable version, the output reports: zero_eq_one : 0 = 1 -- no axioms On a patched version, the kernel rejects the ill-typed inductive. 5. Root Cause ============= Two omissions in the kernel: (a) Projection validation: the kernel does not check that the structure named in a projection matches the type of the value being projected. CWE-843 (Type Confusion). (b) Nested inductive checking: environment::add_inductive does not type-check nested inductive applications, so their parameters go unchecked. CWE-20 (Improper Input Validation). Combined, these allow a metaprogram to register an ill-typed nested inductive that exploits the projection mismatch, producing a closed proof of False. 6. Scoring ========== CVSS 3.1: AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High) 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.8 (Medium) 7. CWE ====== CWE-843: Access of Resource Using Incompatible Type (Type Confusion) CWE-20: Improper Input Validation 8. CVE ====== CVE-2026-72844 (assigned by VulnCheck as CNA) 9. Affected Versions ==================== Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 Fixed in: nightly 2026-07-29 and later; v4.32.2 10. Mitigation ============== - Upgrade to Lean 4 v4.32.2 or later. - No workaround exists for affected versions — the flaw is in the kernel itself. 11. References ============== Bug report: https://github.com/leanprover/lean4/issues/14576 Fix: https://github.com/leanprover/lean4/pull/14577 PoC: https://github.com/endrazine/lean-cve-poc VulnCheck: https://www.vulncheck.com/advisories/lean-4-before-kernel-type-checking-bypa... NVD: https://nvd.nist.gov/vuln/detail/CVE-2026-72844 12. Timeline ============ 2026-07-27 Bug reported (leanprover/lean4#14576) 2026-07-29 Kernel fix merged (PR #14577) 2026-08-02 Advisory posted to oss-security 2026-08-20 CVE-2026-72844 published by VulnCheck 2026-08-24 Docker-reproducible PoC published 13. Credit ========== Bug discovery and minimal PoC: @kiranandcode Original CollatzLean exploit: Ramana Kumar (@xrchz) Kernel fix: Leonardo de Moura PoC packaging: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com

Severity

No CVSS data available.

CWE

Assigner

VULNARCHIVE GNA GNA-1988

GNA scorecard E 38/100 over 556 records in the last 180 days details

References

7 references

URL	Tags
https://vuln.freearchive.org/archive/item/1d180a8…	technical-descriptionexploit
https://lists.securityfocus.com/hyperkitty/list/b…	technical-description
https://github.com/endrazine/lean-cve-poc
https://github.com/leanprover/lean4/issues/14576
https://github.com/leanprover/lean4/pull/14577
https://nvd.nist.gov/vuln/detail/CVE-2026-72844
https://www.vulncheck.com/advisories/lean-4-befor…

Impacted products

1 product

Vendor	Product	Version
leanprover	lean4	Affected: unknown

Credits

Jonathan Brossard

Relationships

analysis GCVE-1988-2026-0441 (this record)

related CVE-2026-72844

JSON

To clipboard

{
  "containers": {
    "cna": {
      "affected": [
        {
          "product": "lean4",
          "vendor": "leanprover",
          "versions": [
            {
              "status": "affected",
              "version": "unknown"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Jonathan Brossard"
        }
      ],
      "descriptions": [
        {
          "lang": "en",
          "value": "1. Summary\n==========\nA soundness bug in the Lean 4 kernel allows construction of a checked\nproof of False \u2014 and by extension, any proposition, including 0 = 1 \u2014\nwithout axioms, sorry, unsafeCast, or modified .olean files.\nThe kernel does not verify that the structure named in a projection\nexpression matches the type of the value being projected. Additionally,\nenvironment::add_inductive in src/kernel/inductive.cpp did not type-check\nnested inductive applications, leaving their parameters unchecked. A\nmetaprogram can register an ill-typed nested inductive and produce a\nproof of False at maximum kernel checking (--trust=0).\nThe proof of concept pads expressions to force hash collisions, defeating\nkernel caching. This is the means of reaching the flaw, not its cause.\n2. Context\n==========\nLean 4 is increasingly used as a foundation for formally verified\nsoftware, proof-carrying code, and mathematical libraries. Its kernel is\nthe trusted core: every theorem must pass kernel type-checking before it\nis accepted. A soundness bug in the kernel undermines the guarantees of\nany system built on top of it.\nFormally verified systems certified under Common Criteria (ISO 15408) or\nDO-178C (airborne software) derive their assurance from the correctness\nof the proof checker. A kernel-level bypass invalidates that assurance\nchain.\nIndependent checkers such as Nanoda and lean4lean replay proofs against\nthe same kernel rules and are therefore equally affected.\n3. Impact\n=========\n- Formally verified software: any proposition can be \"proved\" and\nkernel-checked, including safety properties of compilers, OS kernels,\nand cryptographic libraries.\n- Proof-carrying code: a malicious Lake dependency could inject unsound\ndeclarations that pass kernel checking.\n- Mathematical proof verification: results checked by the Lean kernel\ncannot be trusted on affected versions.\n4. Proof of Concept\n===================\nA Docker-reproducible PoC is available:\ngit clone https://github.com/endrazine/lean-cve-poc\ncd lean-cve-poc\ndocker build -t lean-cve-poc .\ndocker run --rm lean-cve-poc\nOn a vulnerable version, the output reports:\nzero_eq_one : 0 = 1\n-- no axioms\nOn a patched version, the kernel rejects the ill-typed inductive.\n5. Root Cause\n=============\nTwo omissions in the kernel:\n(a) Projection validation: the kernel does not check that the structure\nnamed in a projection matches the type of the value being projected.\nCWE-843 (Type Confusion).\n(b) Nested inductive checking: environment::add_inductive does not\ntype-check nested inductive applications, so their parameters go\nunchecked. CWE-20 (Improper Input Validation).\nCombined, these allow a metaprogram to register an ill-typed nested\ninductive that exploits the projection mismatch, producing a closed\nproof of False.\n6. Scoring\n==========\nCVSS 3.1: AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N \u2014 7.1 (High)\nCVSS 4.0: AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N \u2014 6.8\n(Medium)\n7. CWE\n======\nCWE-843: Access of Resource Using Incompatible Type (Type Confusion)\nCWE-20: Improper Input Validation\n8. CVE\n======\nCVE-2026-72844 (assigned by VulnCheck as CNA)\n9. Affected Versions\n====================\nLean 4 \u2264 v4.31.0 / nightly \u2264 2026-07-27\nFixed in: nightly 2026-07-29 and later; v4.32.2\n10. Mitigation\n==============\n- Upgrade to Lean 4 v4.32.2 or later.\n- No workaround exists for affected versions \u2014 the flaw is in the\nkernel itself.\n11. References\n==============\nBug report:  https://github.com/leanprover/lean4/issues/14576\nFix:         https://github.com/leanprover/lean4/pull/14577\nPoC:         https://github.com/endrazine/lean-cve-poc\nVulnCheck:\nhttps://www.vulncheck.com/advisories/lean-4-before-kernel-type-checking-bypa...\nNVD:         https://nvd.nist.gov/vuln/detail/CVE-2026-72844\n12. Timeline\n============\n2026-07-27  Bug reported (leanprover/lean4#14576)\n2026-07-29  Kernel fix merged (PR #14577)\n2026-08-02  Advisory posted to oss-security\n2026-08-20  CVE-2026-72844 published by VulnCheck\n2026-08-24  Docker-reproducible PoC published\n13. Credit\n==========\nBug discovery and minimal PoC: @kiranandcode\nOriginal CollatzLean exploit:  Ramana Kumar (@xrchz)\nKernel fix:                    Leonardo de Moura\nPoC packaging:                 Jonathan Brossard (@endrazine) \u2014 MOABI /\nPSIRT.com"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-20",
              "description": "CWE-20",
              "lang": "en",
              "type": "CWE"
            },
            {
              "cweId": "CWE-843",
              "description": "CWE-843",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-11-02T07:29:43Z",
        "orgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
        "shortName": "VULNARCHIVE"
      },
      "references": [
        {
          "tags": [
            "technical-description",
            "exploit"
          ],
          "url": "https://vuln.freearchive.org/archive/item/1d180a8302029b1f56d12aff2ae2936067901f43fe12e67588131da7114d6012"
        },
        {
          "tags": [
            "technical-description"
          ],
          "url": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/5APDW5T3SOY76W62O73OGAX7GDRAIXF2/"
        },
        {
          "url": "https://github.com/endrazine/lean-cve-poc"
        },
        {
          "url": "https://github.com/leanprover/lean4/issues/14576"
        },
        {
          "url": "https://github.com/leanprover/lean4/pull/14577"
        },
        {
          "url": "https://nvd.nist.gov/vuln/detail/CVE-2026-72844"
        },
        {
          "url": "https://www.vulncheck.com/advisories/lean-4-before-kernel-type-checking-bypass"
        }
      ],
      "source": {
        "defect": [
          "9374a790-b0c0-4fd2-b81a-f8cd507dc8a1%40gmail.com"
        ],
        "discovery": "EXTERNAL"
      },
      "title": "[Bugtraq] CVE-2026-72844: Lean 4 kernel soundness bug \u2014 forging proofs via nested inductive projections (0 = 1 demonstrated)",
      "x_gcve": [
        {
          "recordType": "analysis",
          "relationships": [
            {
              "destId": "CVE-2026-72844",
              "type": "related"
            }
          ],
          "vulnId": "GCVE-1988-2026-0441",
          "x_vulnarchive": {
            "archiveUrl": "https://vuln.freearchive.org/archive/item/1d180a8302029b1f56d12aff2ae2936067901f43fe12e67588131da7114d6012",
            "automated": true,
            "contentSha256": "1d180a8302029b1f56d12aff2ae2936067901f43fe12e67588131da7114d6012",
            "evidenceScore": 10,
            "messageId": "9374a790-b0c0-4fd2-b81a-f8cd507dc8a1%40gmail.com",
            "originalUrl": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/5APDW5T3SOY76W62O73OGAX7GDRAIXF2/",
            "policy": "vulnarchive-1",
            "sourceFormat": "text/html",
            "sourcePublishedAt": "2026-11-02T07:29:43Z"
          }
        },
        {
          "recordType": "advisory",
          "vulnId": "gcve-1988-2026-0441"
        }
      ]
    }
  },
  "cveMetadata": {
    "assignerOrgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
    "assignerShortName": "VULNARCHIVE",
    "datePublished": "2026-11-02T07:29:43Z",
    "dateUpdated": "2026-11-02T07:29:43Z",
    "state": "PUBLISHED",
    "vulnId": "GCVE-1988-2026-0441"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

GHSA-4FHC-8RQ3-CJVG

Vulnerability from github – Published: 2026-08-20 18:31 – Updated: 2026-10-26 03:30

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-72844"
  ],
  "database_specific": {
    "cwe_ids": [
      "CWE-843"
    ],
    "github_reviewed": false,
    "github_reviewed_at": null,
    "nvd_published_at": "2026-08-20T18:16:45Z",
    "severity": "MODERATE"
  },
  "details": "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.",
  "id": "GHSA-4fhc-8rq3-cjvg",
  "modified": "2026-10-26T03:30:22Z",
  "published": "2026-08-20T18:31:00Z",
  "references": [
    {
      "type": "ADVISORY",
      "url": "https://nvd.nist.gov/vuln/detail/CVE-2026-72844"
    },
    {
      "type": "WEB",
      "url": "https://github.com/leanprover/lean4/issues/14576"
    },
    {
      "type": "WEB",
      "url": "https://github.com/leanprover/lean4/pull/14577"
    },
    {
      "type": "WEB",
      "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808"
    },
    {
      "type": "WEB",
      "url": "https://github.com/endrazine/lean-cve-poc"
    },
    {
      "type": "WEB",
      "url": "https://github.com/leanprover/lean4"
    },
    {
      "type": "WEB",
      "url": "https://github.com/xrchz/CollatzLean"
    },
    {
      "type": "WEB",
      "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1"
    },
    {
      "type": "WEB",
      "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections"
    },
    {
      "type": "WEB",
      "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"
    }
  ],
  "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.

Vulnerability timeline

Sightings and recorded dates, grouped by day · UTC

Order JSON

How durations are calculated

Following the VTEM framework (Black Hat USA 2015), time to patch starts when the vendor or a coordinator was informed, total time to patch at discovery, and disclosure to patch at public disclosure; vendor response time runs from the report to its acknowledgement. Time to exploit and time unpatched start at the earliest discovery or report, falling back to public disclosure. Unpatched time ends at the first recorded patch, or the calculation time when no patch is recorded. Exploitation to patch shows the interval between those two events; a published proof of concept is a public exploit, not exploitation.

Each result shows its source dates. A negative interval means the end event came first; when date-only inputs leave the order open, the result says so. Date-only inputs are approximate. The earliest evidence wins: KEV report dates and sightings are labelled as such. Records describing another vulnerability are listed but never calculated from, and a PoC alone does not establish exploitation. Missing patch evidence does not prove that no patch exists. Filters below change the event list only.

Publication & reservation Sightings KEV catalogs Other timestamps

Loading timeline…

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.
Browse all ATT&CK techniques and the vulnerabilities related to each.

Related by attack behaviour

Vulnerabilities whose description is nearest to this one in the vector space of the CIRCL/vulnerability-attack-technique-biencoder model. This is a similarity search over the bi-encoder space (plain cosine), not a classification, and it has no measured accuracy.

Action not permitted

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

FKIE_CVE-2026-72844

GCVE-1988-2026-0441

GHSA-4FHC-8RQ3-CJVG

Tags

Sightings

Nomenclature

Vulnerability timeline

Related by attack behaviour