CVE-2020-37268Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline
- 6.8MediumCVSS base score
- 0.18%Exploitation in 30 daysEPSS · top 93% of all CVEs
- NoKnown exploitednot in CISA's KEV catalog
- YesPublic exploitsa reference or SSVC says so
Description
Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.
Public exploit
An exploit or proof of concept is public: anyone can try it against an unpatched system. 2 references of the record are tagged as an exploit. CISA's SSVC rates its exploitation: a proof of concept is public.
Show the exploits2
References tagged exploit2 references
Timeline
ID reserved
By VulnCheck
- 5 days later
· 5 days later
Published
- 2 months later
· 2 months later
Record updated
Changes after publication (a new score, a public exploit, EPSS crossing 1, 10 or 50 %, leaving KEV) are kept since November 2026; earlier ones are not known.
Scores
| Scored by | CVSS | Score | Vector |
|---|---|---|---|
| VulnCheckCNA (assigner) | 4.0 | Medium6.8 | 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 |
| VulnCheckCNA (assigner) | 3.1 | Medium6.3 | CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N |
| NVDNVD · Deferred | 4.0 | Medium6.8 | 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 |
- EPSS (exploitation in 30 days)
- 0.18% · top 93% of all CVEs (13 Nov 2026)
- CISA SSVC
- Exploitation: poc · Automatable: no · Technical impact: partial
The list uses the assigner's score when there is one, then CISA's, then NVD's: Medium 6.8.
Affected products
- affected 8.11 – ≤ 9.2.0
References
References6
- https://github.com/rocq-prover/rocq (opens in a new tab)product
- https://github.com/rocq-prover/rocq/issues/12155 (opens in a new tab)issue-trackingexploit
- https://github.com/rocq-prover/rocq/blob/master/dev/doc/critical-bugs.md (opens in a new tab)technical-description
- https://github.com/endrazine/rocq-cve-poc-12155 (opens in a new tab)exploit
- VulnCheck Advisory: Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline (opens in a new tab)third-party-advisory
- http://www.openwall.com/lists/oss-security/2026/10/26/8 (opens in a new tab)
Sources
The same CVE in the primary databases and aggregators, to check against.
- CVE.org record (opens in a new tab)
- CVE List JSON (GitHub) (opens in a new tab)
- NVD (opens in a new tab)
- FIRST EPSS (opens in a new tab)
- EUVD EUVD-2020-31263 (opens in a new tab)
- OSV.dev (opens in a new tab)
- GitHub Advisories (opens in a new tab)
- CIRCL Vulnerability-Lookup (opens in a new tab)
Badge for a README or a ticket
[](https://cveledger.app/cve/CVE-2020-37268)Record last updated .