CVE-2026-72844

{"dataType": "CVE_RECORD", "dataVersion": "5.2", "cveMetadata": {"cveId": "CVE-2026-72844", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "state": "PUBLISHED", "assignerShortName": "VulnCheck", "dateReserved": "2026-08-10T15:14:51.467Z", "datePublished": "2026-08-20T17:19:34.054Z", "dateUpdated": "2026-11-08T14:08:40.851Z"}, "containers": {"cna": {"providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-11-08T14:08:40.851Z"}, "datePublic": "2026-07-28T00:00:00.000Z", "title": "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections", "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."}], "problemTypes": [{"descriptions": [{"lang": "en", "description": "Access of Resource Using Incompatible Type ('Type Confusion')", "cweId": "CWE-843", "type": "CWE"}]}], "affected": [{"vendor": "leanprover", "product": "lean4", "defaultStatus": "unaffected", "repo": "https://github.com/leanprover/lean4", "versions": [{"version": "0", "lessThan": "4.32.2", "status": "affected", "versionType": "semver"}, {"version": "4.32.2", "status": "unaffected", "versionType": "semver"}, {"version": "4.33.0-rc1", "status": "affected", "versionType": "semver"}]}], "metrics": [{"format": "CVSS", "cvssV3_1": {"version": "3.1", "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N", "attackVector": "LOCAL", "attackComplexity": "LOW", "privilegesRequired": "NONE", "userInteraction": "REQUIRED", "scope": "CHANGED", "confidentialityImpact": "NONE", "integrityImpact": "HIGH", "availabilityImpact": "NONE", "baseScore": 6.3, "baseSeverity": "MEDIUM"}}, {"format": "CVSS", "cvssV4_0": {"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", "attackVector": "LOCAL", "attackComplexity": "LOW", "attackRequirements": "NONE", "privilegesRequired": "NONE", "userInteraction": "PASSIVE", "vulnConfidentialityImpact": "NONE", "vulnIntegrityImpact": "HIGH", "vulnAvailabilityImpact": "NONE", "subConfidentialityImpact": "NONE", "subIntegrityImpact": "NONE", "subAvailabilityImpact": "NONE", "baseScore": 6.8, "baseSeverity": "MEDIUM"}}], "references": [{"url": "https://github.com/leanprover/lean4/issues/14576", "tags": ["issue-tracking"], "name": "GitHub Issue #14576"}, {"url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808", "tags": ["patch"], "name": "fix: missing check at kernel inductive declaration"}, {"url": "https://github.com/leanprover/lean4/pull/14577", "tags": ["issue-tracking", "patch"], "name": "GitHub Pull Request #14577"}, {"url": "https://github.com/endrazine/lean-cve-poc", "tags": ["exploit"], "name": "lean-cve-poc"}, {"url": "https://github.com/xrchz/CollatzLean", "tags": ["exploit"], "name": "CollatzLean"}, {"url": "https://www.openwall.com/lists/oss-security/2026/08/02/1", "tags": ["third-party-advisory"], "name": "oss-security: Lean 4 kernel soundness bug"}, {"url": "https://github.com/leanprover/lean4", "tags": ["product"]}, {"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"}], "credits": [{"lang": "en", "value": "kiranandcode", "type": "finder"}, {"lang": "en", "value": "Ramana Kumar (@xrchz)", "type": "other"}, {"lang": "en", "value": "Leonardo de Moura", "type": "remediation developer"}, {"lang": "en", "value": "Jonathan Brossard (MOABI)", "type": "other"}], "x_generator": {"engine": "vulncheck-endgame"}, "timeline": [{"time": "2026-07-25T00:00:00.000Z", "lang": "en", "value": "CollatzLean repository published, exploiting the bug"}, {"time": "2026-07-28T00:00:00.000Z", "lang": "en", "value": "Bug identified and reported in issue #14576"}, {"time": "2026-07-28T00:00:00.000Z", "lang": "en", "value": "Fix submitted in pull request #14577"}, {"time": "2026-07-29T00:00:00.000Z", "lang": "en", "value": "Fix available in nightly builds"}, {"time": "2026-08-02T00:00:00.000Z", "lang": "en", "value": "Public advisory on oss-security"}]}, "adp": [{"metrics": [{"other": {"type": "ssvc", "content": {"timestamp": "2026-08-21T21:13:48.944575Z", "id": "CVE-2026-72844", "options": [{"Exploitation": "poc"}, {"Automatable": "no"}, {"Technical Impact": "partial"}], "role": "CISA Coordinator", "version": "2.0.3"}}}], "title": "CISA ADP Vulnrichment", "providerMetadata": {"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "shortName": "CISA-ADP", "dateUpdated": "2026-08-21T21:46:54.936Z"}}, {"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:59.293Z"}}]}}

{"dataType": "CVE_RECORD", "containers": {"adp": [{"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/2"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:59.293Z"}}, {"title": "CISA ADP Vulnrichment", "metrics": [{"other": {"type": "ssvc", "content": {"id": "CVE-2026-72844", "role": "CISA Coordinator", "options": [{"Exploitation": "poc"}, {"Automatable": "no"}, {"Technical Impact": "partial"}], "version": "2.0.3", "timestamp": "2026-08-21T21:13:48.944575Z"}}}], "providerMetadata": {"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "shortName": "CISA-ADP", "dateUpdated": "2026-08-21T21:13:57.269Z"}}], "cna": {"title": "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections", "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)"}], "metrics": [{"format": "CVSS", "cvssV3_1": {"scope": "CHANGED", "version": "3.1", "baseScore": 6.3, "attackVector": "LOCAL", "baseSeverity": "MEDIUM", "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N", "integrityImpact": "HIGH", "userInteraction": "REQUIRED", "attackComplexity": "LOW", "availabilityImpact": "NONE", "privilegesRequired": "NONE", "confidentialityImpact": "NONE"}}, {"format": "CVSS", "cvssV4_0": {"version": "4.0", "baseScore": 6.8, "attackVector": "LOCAL", "baseSeverity": "MEDIUM", "vectorString": "CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N", "userInteraction": "PASSIVE", "attackComplexity": "LOW", "attackRequirements": "NONE", "privilegesRequired": "NONE", "subIntegrityImpact": "NONE", "vulnIntegrityImpact": "HIGH", "subAvailabilityImpact": "NONE", "vulnAvailabilityImpact": "NONE", "subConfidentialityImpact": "NONE", "vulnConfidentialityImpact": "NONE"}}], "affected": [{"repo": "https://github.com/leanprover/lean4", "vendor": "leanprover", "product": "lean4", "versions": [{"status": "affected", "version": "0", "lessThan": "4.32.2", "versionType": "semver"}, {"status": "unaffected", "version": "4.32.2", "versionType": "semver"}, {"status": "affected", "version": "4.33.0-rc1", "versionType": "semver"}], "defaultStatus": "unaffected"}], "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"}], "datePublic": "2026-07-28T00:00:00.000Z", "references": [{"url": "https://github.com/leanprover/lean4/issues/14576", "name": "GitHub Issue #14576", "tags": ["issue-tracking"]}, {"url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808", "name": "fix: missing check at kernel inductive declaration", "tags": ["patch"]}, {"url": "https://github.com/leanprover/lean4/pull/14577", "name": "GitHub Pull Request #14577", "tags": ["issue-tracking", "patch"]}, {"url": "https://github.com/endrazine/lean-cve-poc", "name": "lean-cve-poc", "tags": ["exploit"]}, {"url": "https://github.com/xrchz/CollatzLean", "name": "CollatzLean", "tags": ["exploit"]}, {"url": "https://www.openwall.com/lists/oss-security/2026/08/02/1", "name": "oss-security: Lean 4 kernel soundness bug", "tags": ["third-party-advisory"]}, {"url": "https://github.com/leanprover/lean4", "tags": ["product"]}, {"url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections", "name": "VulnCheck Advisory: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections", "tags": ["third-party-advisory"]}], "x_generator": {"engine": "vulncheck-endgame"}, "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."}], "problemTypes": [{"descriptions": [{"lang": "en", "type": "CWE", "cweId": "CWE-843", "description": "Access of Resource Using Incompatible Type ('Type Confusion')"}]}], "providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-11-08T14:08:40.851Z"}}}, "cveMetadata": {"cveId": "CVE-2026-72844", "state": "PUBLISHED", "dateUpdated": "2026-11-08T14:08:40.851Z", "dateReserved": "2026-08-10T15:14:51.467Z", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "datePublished": "2026-08-20T17:19:34.054Z", "assignerShortName": "VulnCheck"}, "dataVersion": "5.2"}

{"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"}]}

{}

{"affected": [{"configurations": [{"platform": null, "status": "affected", "versions": {"scheme": "semver", "value": "[0,4.32.2)"}}, {"platform": null, "status": "unaffected", "versions": {"scheme": "semver", "value": "4.32.2"}}, {"platform": null, "status": "affected", "versions": {"scheme": "semver", "value": "4.33.0-rc1"}}], "enrichment": {"confidence": 100.0, "confidence_source": "cna", "scores": [{"score": 100.0, "source": "cna"}]}, "product": "lean4", "vendor": "leanprover"}], "created": "2026-08-20T20:30:05.829549+00:00", "updated": "2026-08-21T13:01:24.961251+00:00", "vendors": ["leanprover", "leanprover$PRODUCT$lean4"]}