Vulnerability-Lookup

GCVE-1988-2026-0446

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

Title

[Bugtraq] CVE-2026-72714: Rocq universe checking state desynchronised after module close (0 = 1 demonstrated) — 0-day

Summary

1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, plugins, or unsafe flags. Print Assumptions reports the proof as closed under the global context. The module system does not correctly restore the universe checking flag when a module that locally disabled the check (`Local Unset Universe Checking`) is closed. The global flag is restored, but the universe graph keeps its own copy of the flag, which remains disabled. Test Universe Checking reports the check as enabled while the kernel still accepts universe-inconsistent terms. This allows Hurkens' paradox to prove False. This is a 0-day: no fix has been merged as of Rocq 9.2.0. This CVE was used to construct Millennium Problem forgeries — Docker- reproducible certificates "proving" the Riemann Hypothesis, Navier- Stokes regularity, BSD conjecture, and Hodge conjecture, all passing Print Assumptions with a clean axiom whitelist. 2. Context ========== Rocq (formerly Coq) is the reference implementation of the Calculus of Inductive Constructions and one of the most widely deployed proof assistants. Its kernel is the trusted core that checks every proof before acceptance. Universe checking is a critical safety mechanism: without it, Girard's paradox (via Hurkens' construction in the standard library) can derive False. 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. The desynchronisation is particularly dangerous because Test Universe Checking reports the flag as enabled — neither the user nor automated tooling can detect the actual kernel state through the normal query mechanism. 3. Impact ========= - Formally verified compilers (CompCert) - Verified OS kernels (CertiKOS) - Separation logic frameworks (Iris) - Mathematical libraries (MathComp) - Proof-carrying code: a malicious .v file in a dependency could introduce unsound declarations that pass both Print Assumptions and Test Universe Checking - Verified smart contracts (ConCert) - Mathematical proof verification: Millennium Problem forgeries demonstrate that arbitrary mathematical claims can be "certified" 4. Publicly Demonstrated ======================== Millennium Problem forgeries built using this CVE: - Riemann Hypothesis (Lagarias criterion): https://github.com/endrazine/rocq-cve-poc-22287-rh - Navier-Stokes regularity (and its negation): https://github.com/endrazine/rocq-cve-poc-22287-ns - BSD conjecture (rank equality): https://github.com/endrazine/rocq-cve-poc-22287-bsd - Hodge conjecture: https://github.com/endrazine/rocq-cve-poc-22287-hodge - P=NP (by JP Aumasson): https://github.com/endrazine/rocq-cve-poc-22287-pnp All forgeries are Docker-reproducible and print FORGERY CONFIRMED with Print Assumptions whitelist clean. 5. Proof of Concept =================== A Docker-reproducible PoC is available: git clone https://github.com/endrazine/rocq-cve-poc-22287 cd rocq-cve-poc-22287 docker build -t rocq-cve-poc-22287 . docker run --rm rocq-cve-poc-22287 On Rocq ≤9.2.0, the output confirms the proof of 0 = 1 with no axioms and Test Universe Checking reporting "on" while the kernel accepts universe-inconsistent terms. 6. Root Cause ============= When a module executes Local Unset Universe Checking, the global environment's flag is correctly scoped and restored on module close. However, the universe graph maintains its own copy of the flag, and module close does not synchronise this copy. The graph's flag remains disabled after the module closes. (a) CWE-459: Incomplete Cleanup — the module close does not clean up the universe graph's copy of the flag. (b) CWE-20: Improper Input Validation — the kernel accepts universe- inconsistent terms based on the stale flag value. 7. 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) 8. CWE ====== CWE-459: Incomplete Cleanup CWE-20: Improper Input Validation 9. CVE ====== CVE-2026-72714 (assigned by VulnCheck as CNA) 10. Affected Versions ===================== Rocq Prover ≤ 9.2.0 (all versions including Coq 8.x that include Hurkens in the standard library) Fixed in: UNFIXED as of Rocq 9.2.0. 11. Mitigation ============== - No patched version is available. - Run coqchk on compiled .vo files — coqchk operates independently of the in-process flag state. - Audit dependencies for use of Local Unset Universe Checking inside modules. - Do not rely on Test Universe Checking to verify kernel state after module operations. 12. References ============== Bug report: https://github.com/rocq-prover/rocq/issues/22287 PoC: https://github.com/endrazine/rocq-cve-poc-22287 VulnCheck: https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-s... NVD: https://nvd.nist.gov/vuln/detail/CVE-2026-72714 13. Timeline ============ 2026 Bug reported by Gaëtan Gilbert (rocq-prover/rocq#22287) 2026 Issue remains open — no fix merged 2026-08-24 CVE-2026-72714 published by VulnCheck 2026-08-24 Docker-reproducible PoC published 2026-08 Millennium Problem forgeries published 14. Credit ========== Bug discovery: Gaëtan Gilbert (@SkySkimmer) P=NP forgery: JP Aumasson (@veorq) 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

11 references

URL	Tags
https://vuln.freearchive.org/archive/item/804f4ce…	technical-descriptionexploit
https://lists.securityfocus.com/hyperkitty/list/b…	technical-description
https://github.com/endrazine/rocq-cve-poc-22287
https://github.com/endrazine/rocq-cve-poc-22287-bsd
https://github.com/endrazine/rocq-cve-poc-22287-hodge
https://github.com/endrazine/rocq-cve-poc-22287-ns
https://github.com/endrazine/rocq-cve-poc-22287-pnp
https://github.com/endrazine/rocq-cve-poc-22287-rh
https://github.com/rocq-prover/rocq/issues/22287
https://nvd.nist.gov/vuln/detail/CVE-2026-72714
https://www.vulncheck.com/advisories/rocq-prover-…

Impacted products

1 product

Vendor	Product	Version	CPE status
rocq-prover	rocq	Affected: unknown	guessed

Credits

Jonathan Brossard

Relationships

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

related CVE-2026-72714

JSON

To clipboard

{
  "containers": {
    "cna": {
      "affected": [
        {
          "product": "rocq",
          "vendor": "rocq-prover",
          "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 Rocq (formerly Coq) kernel allows construction\nof a checked proof of False \u2014 and by extension, any proposition,\nincluding 0 = 1 \u2014 without axioms, plugins, or unsafe flags. Print\nAssumptions reports the proof as closed under the global context.\nThe module system does not correctly restore the universe checking flag\nwhen a module that locally disabled the check (`Local Unset Universe\nChecking`) is closed. The global flag is restored, but the universe\ngraph keeps its own copy of the flag, which remains disabled. Test\nUniverse Checking reports the check as enabled while the kernel still\naccepts universe-inconsistent terms. This allows Hurkens\u0027 paradox to\nprove False.\nThis is a 0-day: no fix has been merged as of Rocq 9.2.0.\nThis CVE was used to construct Millennium Problem forgeries \u2014 Docker-\nreproducible certificates \"proving\" the Riemann Hypothesis, Navier-\nStokes regularity, BSD conjecture, and Hodge conjecture, all passing\nPrint Assumptions with a clean axiom whitelist.\n2. Context\n==========\nRocq (formerly Coq) is the reference implementation of the Calculus of\nInductive Constructions and one of the most widely deployed proof\nassistants. Its kernel is the trusted core that checks every proof\nbefore acceptance. Universe checking is a critical safety mechanism:\nwithout it, Girard\u0027s paradox (via Hurkens\u0027 construction in the standard\nlibrary) can derive False.\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.\nThe desynchronisation is particularly dangerous because Test Universe\nChecking reports the flag as enabled \u2014 neither the user nor automated\ntooling can detect the actual kernel state through the normal query\nmechanism.\n3. Impact\n=========\n- Formally verified compilers (CompCert)\n- Verified OS kernels (CertiKOS)\n- Separation logic frameworks (Iris)\n- Mathematical libraries (MathComp)\n- Proof-carrying code: a malicious .v file in a dependency could\nintroduce unsound declarations that pass both Print Assumptions and\nTest Universe Checking\n- Verified smart contracts (ConCert)\n- Mathematical proof verification: Millennium Problem forgeries\ndemonstrate that arbitrary mathematical claims can be \"certified\"\n4. Publicly Demonstrated\n========================\nMillennium Problem forgeries built using this CVE:\n- Riemann Hypothesis (Lagarias criterion):\nhttps://github.com/endrazine/rocq-cve-poc-22287-rh\n- Navier-Stokes regularity (and its negation):\nhttps://github.com/endrazine/rocq-cve-poc-22287-ns\n- BSD conjecture (rank equality):\nhttps://github.com/endrazine/rocq-cve-poc-22287-bsd\n- Hodge conjecture:\nhttps://github.com/endrazine/rocq-cve-poc-22287-hodge\n- P=NP (by JP Aumasson):\nhttps://github.com/endrazine/rocq-cve-poc-22287-pnp\nAll forgeries are Docker-reproducible and print FORGERY CONFIRMED with\nPrint Assumptions whitelist clean.\n5. Proof of Concept\n===================\nA Docker-reproducible PoC is available:\ngit clone https://github.com/endrazine/rocq-cve-poc-22287\ncd rocq-cve-poc-22287\ndocker build -t rocq-cve-poc-22287 .\ndocker run --rm rocq-cve-poc-22287\nOn Rocq \u22649.2.0, the output confirms the proof of 0 = 1 with no axioms\nand Test Universe Checking reporting \"on\" while the kernel accepts\nuniverse-inconsistent terms.\n6. Root Cause\n=============\nWhen a module executes Local Unset Universe Checking, the global\nenvironment\u0027s flag is correctly scoped and restored on module close.\nHowever, the universe graph maintains its own copy of the flag, and\nmodule close does not synchronise this copy. The graph\u0027s flag remains\ndisabled after the module closes.\n(a) CWE-459: Incomplete Cleanup \u2014 the module close does not clean up\nthe universe graph\u0027s copy of the flag.\n(b) CWE-20: Improper Input Validation \u2014 the kernel accepts universe-\ninconsistent terms based on the stale flag value.\n7. 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)\n8. CWE\n======\nCWE-459: Incomplete Cleanup\nCWE-20: Improper Input Validation\n9. CVE\n======\nCVE-2026-72714 (assigned by VulnCheck as CNA)\n10. Affected Versions\n=====================\nRocq Prover \u2264 9.2.0 (all versions including Coq 8.x that include\nHurkens in the standard library)\nFixed in: UNFIXED as of Rocq 9.2.0.\n11. Mitigation\n==============\n- No patched version is available.\n- Run coqchk on compiled .vo files \u2014 coqchk operates independently of\nthe in-process flag state.\n- Audit dependencies for use of Local Unset Universe Checking inside\nmodules.\n- Do not rely on Test Universe Checking to verify kernel state after\nmodule operations.\n12. References\n==============\nBug report:  https://github.com/rocq-prover/rocq/issues/22287\nPoC:         https://github.com/endrazine/rocq-cve-poc-22287\nVulnCheck:\nhttps://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-s...\nNVD:         https://nvd.nist.gov/vuln/detail/CVE-2026-72714\n13. Timeline\n============\n2026        Bug reported by Ga\u00ebtan Gilbert (rocq-prover/rocq#22287)\n2026        Issue remains open \u2014 no fix merged\n2026-08-24  CVE-2026-72714 published by VulnCheck\n2026-08-24  Docker-reproducible PoC published\n2026-08     Millennium Problem forgeries published\n14. Credit\n==========\nBug discovery:   Ga\u00ebtan Gilbert (@SkySkimmer)\nP=NP forgery:    JP Aumasson (@veorq)\nPoC packaging:   Jonathan Brossard (@endrazine) \u2014 MOABI / PSIRT.com"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-20",
              "description": "CWE-20",
              "lang": "en",
              "type": "CWE"
            },
            {
              "cweId": "CWE-459",
              "description": "CWE-459",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-11-02T07:29:47Z",
        "orgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
        "shortName": "VULNARCHIVE"
      },
      "references": [
        {
          "tags": [
            "technical-description",
            "exploit"
          ],
          "url": "https://vuln.freearchive.org/archive/item/804f4ce049d531fd5600156172b2094c5c2eb8969c849a6b941ee502c3c4e9e8"
        },
        {
          "tags": [
            "technical-description"
          ],
          "url": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/YAAUNKGUH3IC5JJ2IXKETMPGTNEG32QV/"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287-bsd"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287-hodge"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287-ns"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287-pnp"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22287-rh"
        },
        {
          "url": "https://github.com/rocq-prover/rocq/issues/22287"
        },
        {
          "url": "https://nvd.nist.gov/vuln/detail/CVE-2026-72714"
        },
        {
          "url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close"
        }
      ],
      "source": {
        "defect": [
          "459a018a-ef5a-4549-979a-60235c64d264%40gmail.com"
        ],
        "discovery": "EXTERNAL"
      },
      "title": "[Bugtraq] CVE-2026-72714: Rocq universe checking state desynchronised after module close (0 = 1 demonstrated) \u2014 0-day",
      "x_gcve": [
        {
          "recordType": "analysis",
          "relationships": [
            {
              "destId": "CVE-2026-72714",
              "type": "related"
            }
          ],
          "vulnId": "GCVE-1988-2026-0446",
          "x_vulnarchive": {
            "archiveUrl": "https://vuln.freearchive.org/archive/item/804f4ce049d531fd5600156172b2094c5c2eb8969c849a6b941ee502c3c4e9e8",
            "automated": true,
            "contentSha256": "804f4ce049d531fd5600156172b2094c5c2eb8969c849a6b941ee502c3c4e9e8",
            "evidenceScore": 10,
            "messageId": "459a018a-ef5a-4549-979a-60235c64d264%40gmail.com",
            "originalUrl": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/YAAUNKGUH3IC5JJ2IXKETMPGTNEG32QV/",
            "policy": "vulnarchive-1",
            "sourceFormat": "text/html",
            "sourcePublishedAt": "2026-11-02T07:29:47Z"
          }
        },
        {
          "recordType": "advisory",
          "vulnId": "gcve-1988-2026-0446"
        }
      ]
    }
  },
  "cveMetadata": {
    "assignerOrgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
    "assignerShortName": "VULNARCHIVE",
    "datePublished": "2026-11-02T07:29:47Z",
    "dateUpdated": "2026-11-02T07:29:47Z",
    "state": "PUBLISHED",
    "vulnId": "GCVE-1988-2026-0446"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

CVE-2026-72714 (GCVE-0-2026-72714)

Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-10-26 01:23

Title

Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

Summary

Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available.

Severity

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

6.3 (Medium)


                        
                          CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

SSVC

Exploitation: poc Automatable: no Technical Impact: partial

CISA Coordinator · CISA-ADP (v2.0.3)

Decision recorded 2026-08-25 17:41 UTC

CWE

CWE-459 - Incomplete Cleanup

Assigner

VulnCheck CNA under the mitre root

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

References

5 references

URL	Tags
https://github.com/rocq-prover/rocq	product
https://github.com/rocq-prover/rocq/issues/22287	issue-tracking
https://github.com/endrazine/rocq-cve-poc-22287	exploit
https://www.vulncheck.com/advisories/rocq-prover-…	third-party-advisory
http://www.openwall.com/lists/oss-security/2026/10/26/7

Impacted products

1 product

Vendor	Product	Version
rocq-prover	rocq	Affected: 0 , ≤ 9.2.0 (custom)

Date Public

2026-07-16 00:00

Credits

Gaëtan Gilbert Jonathan Brossard (MOABI)

Show details on NVD website

JSON

To clipboard

{
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-72714",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-25T17:41:19.106957Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-25T17:41:24.594Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "references": [
          {
            "tags": [
              "exploit"
            ],
            "url": "https://github.com/rocq-prover/rocq/issues/22287"
          }
        ],
        "title": "CISA ADP Vulnrichment"
      },
      {
        "providerMetadata": {
          "dateUpdated": "2026-10-26T01:23:58.366Z",
          "orgId": "af854a3a-2127-422b-91ae-364da2661108",
          "shortName": "CVE"
        },
        "references": [
          {
            "url": "http://www.openwall.com/lists/oss-security/2026/10/26/7"
          }
        ],
        "title": "CVE Program Container"
      }
    ],
    "cna": {
      "affected": [
        {
          "defaultStatus": "unaffected",
          "packageURL": "pkg:github/rocq-prover/rocq",
          "product": "rocq",
          "repo": "https://github.com/rocq-prover/rocq",
          "vendor": "rocq-prover",
          "versions": [
            {
              "lessThanOrEqual": "9.2.0",
              "status": "affected",
              "version": "0",
              "versionType": "custom"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Ga\u00ebtan Gilbert"
        },
        {
          "lang": "en",
          "type": "finder",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2026-07-16T00:00:00.000Z",
      "descriptions": [
        {
          "lang": "en",
          "value": "Rocq Prover does not restore the universe graph\u0027s copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens\u0027 paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available."
        }
      ],
      "metrics": [
        {
          "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"
        },
        {
          "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"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-459",
              "description": "Incomplete Cleanup",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-09-24T14:18:54.618Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/rocq-prover/rocq"
        },
        {
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/rocq-prover/rocq/issues/22287"
        },
        {
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/rocq-cve-poc-22287"
        },
        {
          "name": "VulnCheck Advisory: Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close"
        }
      ],
      "title": "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2026-72714",
    "datePublished": "2026-08-24T20:08:33.917Z",
    "dateReserved": "2026-08-10T13:02:52.001Z",
    "dateUpdated": "2026-10-26T01:23:58.366Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2"
}

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