CVE-2026-72711

MEDIUMPre-NVD 6.36.3
EchelonGraph scoreMEDIUM confidence

“—” beside the score: it is equal to the CVSS score beside it.

Score 6.3 from GitHub Security Advisory published 2026-08-24. A secondary CVSS source baseline 6.3; sources differ by 0.0.

Triggered by: GitHub Security Advisory CVSS
Sources: EPSS, GitHub Security Advisory, a secondary CVSS source
Trending — 3 sources updated this weekElevated
6.3EG
EchelonGraph verdictPlan mitigationRemediate within your standard update timelines (the SSVC decision on this page).
  • CISA's Vulnrichment rates exploitation as PoC; EchelonGraph holds no exploit-code reference for it
CISA-KEV: Not listedEPSS PROB: 0.2%CVSS: 6.3Exploit: No code on recordExposed services: Not assessed

An upstream fix is merged but not yet released — mitigate (WAF / firewall / segmentation) until the release ships, then apply it.

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.

CVSS v3
6.3
EG Score
6.3MEDIUMmedium confidence
EG Risk
44
EG Risk 44/100

EG Risk is EchelonGraph's 0–100 priority score: it fuses intrinsic severity with real-world exploitation and automatability so you can rank equal-severity CVEs and fix the most dangerous first. Higher = act sooner. Distinct from the 0–10 EG Score (severity).

How it’s computed (value × EchelonGraph’s weight)
Severity63% × 45%
The EG Score, 6.3 of 10.
Exploitation40% × 40%
EchelonGraph's fixed weight for EG-KEV Tier 3 (Elevated): a constant, not a probability.
Automatability0% × 15%
CISA's SSVC Automatable value: no (Vulnrichment).
SSVC (CISA's decision table, applied by EchelonGraph): Track at low or medium mission impact; Track* at high (mission-essential systems).
Exploitation public PoC (CISA Vulnrichment) · Automatable no (CISA Vulnrichment) · Technical impact partial (CISA Vulnrichment). All three are CISA's SSVC values (Vulnrichment). EchelonGraph applied CISA's decision table to them; CISA publishes SSVC inputs and the table, not a decision for each CVE.
Action: An upstream fix is merged but not yet in a tagged release. Restrict network exposure of the affected system or apply the vendor's mitigation within your standard update timelines until it ships, then apply the release.
EPSS PROB
0.2%
EPSS %ILE
6th
KEV
Not listed

SSVC (CISA's decision table, applied by EchelonGraph)Track at low or medium mission impact; Track* at high (mission-essential systems).

An upstream fix is merged but not yet in a tagged release. Restrict network exposure of the affected system or apply the vendor's mitigation within your standard update timelines until it ships, then apply the release.

Exploitation public PoC (CISA Vulnrichment) · Automatable no (CISA Vulnrichment) · Technical impact partial (CISA Vulnrichment). All three are CISA's SSVC values (Vulnrichment). EchelonGraph applied CISA's decision table to them; CISA publishes SSVC inputs and the table, not a decision for each CVE. Mission impact is CISA's Mission & Well-being decision point, and only you can judge it. CISA's table makes it high when Mission Prevalence is Essential — the vulnerable component "directly provides capabilities that constitute at least one MEF for at least one entity" (MEF: mission essential function) — or when Public Well-Being Impact is Irreversible: "multiple fatalities are likely", the cyber-physical system "is likely lost or destroyed", "extreme or serious externalities" are imposed on other parties, or social systems such as elections or the financial grid "are destabilized and potentially collapse". CISA's decision table

BOD 26-04 (CISA's remediation timeline, Table 1)60 days if the affected system is publicly exposed; Fix on system upgrade if it is not.

In CISA KEV no (CISA's KEV catalog) · Automatable no (CISA Vulnrichment) · Technical impact partial (CISA Vulnrichment). Whether your system is publicly exposed is yours to answer. BOD 26-04 binds US Federal Civilian Executive Branch agencies; for anyone else it is CISA's published timeline, a reference rather than an obligation. The directive · how EchelonGraph applies it

Published

August 24, 2026

Last Modified

October 12, 2026

Advisory Details (5)

Auto-updated Aug 24, 2026
Upstream fix merged — awaiting tagged release. Sources: github_pr.
Web page

Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable | Advisories | VulnCheck

https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable
GitHub pull request

fix: kernel to check opaque values for fvars

Fix merged in leanprover/lean4 PR #14498 on 2026-07-22 — awaiting tagged release

https://github.com/leanprover/lean4/pull/14498
Web page

Missing check apparently allows proof of False after adversarial metaprogram · Issue #14484 · leanprover/lean4 · GitHub

https://github.com/leanprover/lean4/issues/14484
Web page

GitHub - leanprover/lean4: Lean 4 programming language and theorem prover · GitHub

https://github.com/leanprover/lean4
Web page

GitHub - endrazine/lean-cve-poc-14484 · GitHub

https://github.com/endrazine/lean-cve-poc-14484

Vendor Advisories for CVE-2026-72711(1)

These vendors published their own advisory mentioning this CVE — often with vendor-specific remediation steps + affected product lists not in NVD.

Weakness Classification(1)

MITRE Common Weakness Enumeration — the root-cause categories this CVE belongs to.

Data Freshness Timeline

(refreshed 18× in last 7d / 72× in last 30d)

Each row is a time one of our pipelines fetched, updated or re-scored this CVE. For example, "NVD update" means NVD published or revised its analysis for this CVE; "MITRE cvelistV5" means we ingested or refreshed it from the CNA feed. An arrow marks a change the record states ("CVSS v3 → 9.1"); EPSS and GHSA rows show the values recorded at that time, not what changed (EPSS values are rounded; hover one for the exact figures). Most recent first.

Showing the most recent 100 of 130 refreshes on record for this CVE.

A repeat, a row identical to one the same pipeline wrote less than 10 seconds earlier, is not a separate refresh and is not counted. None are among the latest 100 rows. The 30 oldest rows on record are not shown and were not checked, so the counts can still include repeats.

  1. 2026-10-13 16:35 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  2. 2026-10-12 16:34 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  3. 2026-10-12 15:29 UTCEG score recompute
  4. 2026-10-12 15:29 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  5. 2026-10-11 19:27 UTCEG score recompute
  6. 2026-10-11 16:42 UTCEG score recompute
  7. 2026-10-11 14:02 UTCEG score recompute
  8. 2026-10-11 13:49 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  9. 2026-10-10 20:00 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  10. 2026-10-10 12:30 UTCEG score recompute
  11. 2026-10-10 12:30 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  12. 2026-10-09 20:07 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  13. 2026-10-09 05:36 UTCEG score recompute
  14. 2026-10-09 05:36 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  15. 2026-10-08 17:13 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  16. 2026-10-08 04:42 UTCEG score recompute
  17. 2026-10-08 04:42 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  18. 2026-10-07 23:48 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  19. 2026-10-07 03:48 UTCEG score recompute
  20. 2026-10-07 03:48 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  21. 2026-10-06 15:18 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  22. 2026-10-06 02:46 UTCEG score recompute
  23. 2026-10-06 02:46 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  24. 2026-10-05 17:43 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  25. 2026-10-04 23:22 UTCEPSS rescoreEPSS 0.2% · 6th percentile
Show 75 more
  1. 2026-10-04 20:41 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  2. 2026-10-03 16:30 UTCEG score recompute
  3. 2026-10-03 16:30 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  4. 2026-10-03 14:26 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  5. 2026-10-02 08:45 UTCEG score recompute
  6. 2026-10-02 08:45 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  7. 2026-10-01 19:50 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  8. 2026-10-01 07:52 UTCEG score recompute
  9. 2026-10-01 07:52 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  10. 2026-09-30 06:59 UTCEG score recompute
  11. 2026-09-30 06:59 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  12. 2026-09-29 00:02 UTCEG score recompute
  13. 2026-09-29 00:02 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  14. 2026-09-28 13:52 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  15. 2026-09-27 23:09 UTCEG score recompute
  16. 2026-09-27 23:09 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  17. 2026-09-27 13:48 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  18. 2026-09-26 22:16 UTCEG score recompute
  19. 2026-09-26 22:16 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  20. 2026-09-26 15:59 UTCEPSS rescoreEPSS 0.2% · 6th percentile
  21. 2026-09-24 21:20 UTCEG score recompute
  22. 2026-09-24 21:20 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  23. 2026-09-24 14:45 UTCEG score recompute
  24. 2026-09-24 14:45 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  25. 2026-09-23 17:54 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  26. 2026-09-23 13:51 UTCEG score recompute
  27. 2026-09-23 13:51 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  28. 2026-09-22 12:58 UTCEG score recompute
  29. 2026-09-22 12:58 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  30. 2026-09-21 21:09 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  31. 2026-09-21 12:05 UTCEG score recompute
  32. 2026-09-21 12:05 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  33. 2026-09-20 20:16 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  34. 2026-09-20 11:12 UTCEG score recompute
  35. 2026-09-20 11:12 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  36. 2026-09-19 10:18 UTCEG score recompute
  37. 2026-09-19 10:18 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  38. 2026-09-18 19:28 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  39. 2026-09-18 09:25 UTCEG score recompute
  40. 2026-09-18 09:25 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  41. 2026-09-17 08:31 UTCEG score recompute
  42. 2026-09-17 08:31 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  43. 2026-09-16 14:08 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  44. 2026-09-16 07:37 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  45. 2026-09-15 06:41 UTCEG score recompute
  46. 2026-09-15 06:41 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  47. 2026-09-15 03:12 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  48. 2026-09-14 05:47 UTCEG score recompute
  49. 2026-09-14 05:47 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  50. 2026-09-13 04:54 UTCEG score recompute
  51. 2026-09-13 04:54 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  52. 2026-09-12 15:02 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  53. 2026-09-12 04:01 UTCEG score recompute
  54. 2026-09-12 04:01 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  55. 2026-09-11 14:53 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  56. 2026-09-11 03:07 UTCEG score recompute
  57. 2026-09-11 03:07 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  58. 2026-09-10 09:35 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  59. 2026-09-10 02:14 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  60. 2026-09-09 01:21 UTCEG score recompute
  61. 2026-09-09 01:21 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  62. 2026-09-08 22:01 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  63. 2026-09-07 20:34 UTCEG score recompute
  64. 2026-09-07 20:34 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  65. 2026-09-06 19:41 UTCEG score recompute
  66. 2026-09-06 19:40 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  67. 2026-09-06 13:48 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  68. 2026-09-05 18:45 UTCEG score recompute
  69. 2026-09-05 18:45 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  70. 2026-09-04 17:52 UTCEG score recompute
  71. 2026-09-04 17:52 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  72. 2026-09-04 05:07 UTCEPSS rescoreEPSS 0.1% · 2nd percentile
  73. 2026-09-03 16:58 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3
  74. 2026-09-02 16:02 UTCEG score recompute
  75. 2026-09-02 16:01 UTCGHSA enrichmentGHSA-fhmq-xvc2-q54h · GitHub CVSS 6.3

Related CVEs(same CWE)

Frequently asked(5)

What is CVE-2026-72711?
CVE-2026-72711 is a medium-severity vulnerability; its CVE record was published on August 24, 2026. The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::addopaque omits the checknometavarno_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A…
When was CVE-2026-72711 made public?
CVE-2026-72711 was made public on July 22, 2026: that is the date its CVE record's CNA, VulnCheck, gives for when the vulnerability was made public. The CVE record itself was published on August 24, 2026. EchelonGraph's copy of the record carries a last-modified date of October 12, 2026; the record at its source may have been updated since.
Is CVE-2026-72711 actively exploited?
CVE-2026-72711 is not currently on CISA's Known Exploited Vulnerabilities catalog. FIRST EPSS estimates a 0.2% probability of exploitation in the next 30 days (6th percentile of EPSS-scored CVEs).
What is the CVSS score of CVE-2026-72711?
CVE-2026-72711 has a CVSS base score of 6.3 (a secondary CVSS source that NVD displays; NVD's own analysis pending).
How do I remediate CVE-2026-72711?
An upstream fix for CVE-2026-72711 has been merged but is not yet in a tagged release. Until it ships, restrict network exposure of the affected system or apply the vendor's mitigation, then update to the release that contains the fix. The vendor advisories EchelonGraph has for CVE-2026-72711 are linked in the Vendor Advisories panel on this page.

Dependency Blast Radius

Explore the affected products and dependency analysis for CVE-2026-72711

Explore →

Is Your Infrastructure Affected by CVE-2026-72711?

EchelonGraph automatically scans your cloud infrastructure and maps CVE exposure using blast radius analysis.

Book a Demo →Browse All CVEs