GCVE-1988-2026-0441

Vulnerability from gna-1988 – Published: 2026-11-02 07:29 – Updated: 2026-11-02 07:29
VLAI
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
Impacted products
Vendor Product Version CPE status
leanprover lean4 Affected: unknown
guessed Create a notification for this product.
Credits
Jonathan Brossard
Relationships
analysis GCVE-1988-2026-0441 (this record)
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"
}



Log in or create an account to share your comment.




Tags
Taxonomy of the tags.




Drag nodes to arrange them. Double-click a related vulnerability to open it, or a source to visit its link. The Physics button on the left tunes the layout and the simulation; the legend at the bottom left hides or shows nodes by kind and by sighting type.

Forecast uses a logistic model when the trend is rising, or an exponential decay model when the trend is falling. Fitted via linearized least squares.

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

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.

Loading timeline…




    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.