CVE-2026-72844

Full vulnerability record from the local CVENow database.

Description

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

MEDIUM

CVSS score

6.8 (v4.0)

Vulnerability status

Deferred

Source identifier

[email protected]

Published

2026-08-20 18:16:45.290000

Last modified

2026-10-26 02:17:07.847000

View original CVE JSON

{
  "id": "CVE-2026-72844",
  "sourceIdentifier": "[email protected]",
  "published": "2026-08-20T18:16:45.290",
  "lastModified": "2026-10-26T02:17:07.847",
  "vulnStatus": "Deferred",
  "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ón de proyección coincida con el tipo del valor que se está proyectando, y environment::add_inductive en src/kernel/inductive.cpp no comprobó el tipo de las aplicaciones inductivas anidadas que son reemplazadas por tipos auxiliares, por lo que sus argumentos paramétricos escaparon a la verificación. Un metaprograma ejecutándose en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyección .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaración a través de la ruta addDecl comprobada ordinaria con la máxima verificación del kernel, sin sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, o un archivo .olean modificado. El resultado es una confusión de tipos que produce una prueba de Falso que no conlleva axiomas, de la cual se puede derivar cualquier proposición. La prueba de concepto publicada además rellena dos expresiones hasta que sus hashes y profundidades aproximadas colisionan, lo que anula el almacenamiento en caché del kernel; esa es la técnica utilizada para alcanzar la falla, no su causa. La explotación requiere ejecutar un metaprograma en proceso, por ejemplo, construyendo un proyecto o importando una dependencia maliciosa de Lake."
    }
  ],
  "affected": [
    {
      "source": "[email protected]",
      "affectedData": [
        {
          "vendor": "leanprover",
          "product": "lean4",
          "defaultStatus": "unaffected",
          "repo": "https://github.com/leanprover/lean4",
          "versions": [
            {
              "version": "0",
              "lessThan": "4.32.2",
              "versionType": "semver",
              "status": "affected"
            },
            {
              "version": "4.32.2",
              "versionType": "semver",
              "status": "unaffected"
            },
            {
              "version": "4.33.0-rc1",
              "versionType": "semver",
              "status": "affected"
            }
          ]
        }
      ]
    }
  ],
  "metrics": {
    "cvssMetricV40": [
      {
        "source": "[email protected]",
        "type": "Secondary",
        "cvssData": {
          "version": "4.0",
          "vectorString": "CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X",
          "baseScore": 6.8,
          "baseSeverity": "MEDIUM",
          "attackVector": "LOCAL",
          "attackComplexity": "LOW",
          "attackRequirements": "NONE",
          "privilegesRequired": "NONE",
          "userInteraction": "PASSIVE",
          "vulnConfidentialityImpact": "NONE",
          "vulnIntegrityImpact": "HIGH",
          "vulnAvailabilityImpact": "NONE",
          "subConfidentialityImpact": "NONE",
          "subIntegrityImpact": "NONE",
          "subAvailabilityImpact": "NONE",
          "exploitMaturity": "NOT_DEFINED",
          "confidentialityRequirement": "NOT_DEFINED",
          "integrityRequirement": "NOT_DEFINED",
          "availabilityRequirement": "NOT_DEFINED",
          "modifiedAttackVector": "NOT_DEFINED",
          "modifiedAttackComplexity": "NOT_DEFINED",
          "modifiedAttackRequirements": "NOT_DEFINED",
          "modifiedPrivilegesRequired": "NOT_DEFINED",
          "modifiedUserInteraction": "NOT_DEFINED",
          "modifiedVulnConfidentialityImpact": "NOT_DEFINED",
          "modifiedVulnIntegrityImpact": "NOT_DEFINED",
          "modifiedVulnAvailabilityImpact": "NOT_DEFINED",
          "modifiedSubConfidentialityImpact": "NOT_DEFINED",
          "modifiedSubIntegrityImpact": "NOT_DEFINED",
          "modifiedSubAvailabilityImpact": "NOT_DEFINED",
          "Safety": "NOT_DEFINED",
          "Automatable": "NOT_DEFINED",
          "Recovery": "NOT_DEFINED",
          "valueDensity": "NOT_DEFINED",
          "vulnerabilityResponseEffort": "NOT_DEFINED",
          "providerUrgency": "NOT_DEFINED"
        }
      }
    ],
    "cvssMetricV31": [
      {
        "source": "[email protected]",
        "type": "Secondary",
        "cvssData": {
          "version": "3.1",
          "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
          "baseScore": 6.3,
          "baseSeverity": "MEDIUM",
          "attackVector": "LOCAL",
          "attackComplexity": "LOW",
          "privilegesRequired": "NONE",
          "userInteraction": "REQUIRED",
          "scope": "CHANGED",
          "confidentialityImpact": "NONE",
          "integrityImpact": "HIGH",
          "availabilityImpact": "NONE"
        },
        "exploitabilityScore": 1.8,
        "impactScore": 4.0
      }
    ],
    "ssvcV203": [
      {
        "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
        "ssvcData": {
          "timestamp": "2026-08-21T21:13:48.944575Z",
          "id": "CVE-2026-72844",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "partial"
            }
          ],
          "role": "CISA Coordinator",
          "version": "2.0.3"
        }
      }
    ]
  },
  "weaknesses": [
    {
      "source": "[email protected]",
      "type": "Secondary",
      "description": [
        {
          "lang": "en",
          "value": "CWE-843"
        }
      ]
    }
  ],
  "references": [
    {
      "url": "https://github.com/endrazine/lean-cve-poc",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/leanprover/lean4",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/leanprover/lean4/issues/14576",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/leanprover/lean4/pull/14577",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/xrchz/CollatzLean",
      "source": "[email protected]"
    },
    {
      "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1",
      "source": "[email protected]"
    },
    {
      "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections",
      "source": "[email protected]"
    },
    {
      "url": "http://www.openwall.com/lists/oss-security/2026/10/26/2",
      "source": "af854a3a-2127-422b-91ae-364da2661108"
    }
  ]
}