rocq-prover has 5 CVEs on record. 5 were published in the last 90 days. The busiest recent month was August 2026 with 5. The median CVSS is 6.3 (medium). None have a confirmed exploitation report. The most common weakness class is CWE-670 (3).
CVEs per month
Last 12 months, by publish date
- Exploited share
- 0% vs 1% corpus
- Median CVSS
- 6.3
- Publish → KEV
- —
- Last 90 days
- 5 prev 0
Worst active — by depth score
CVE-2026-72714Medium· 6.3Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed47CVE-2026-72705Medium· 6.3The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments47CVE-2026-72704Medium· 6.3The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport47CVE-2026-72703Medium· 6.3The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint47CVE-2020-37268Medium· 6.3Print 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 type47
rocq-prover vulnerabilities
CVEs affecting rocq-prover, newest first. Open any entry for full detail, references, and exploit status.
5 CVEsRSS
CVE-2026-72714Medium· 6.3PoCRocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed
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, a…
CVE-2026-72705Medium· 6.3PoCThe guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm …
CVE-2026-72704Medium· 6.3PoCThe guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport
The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its …
CVE-2026-72703Medium· 6.3PoCThe guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive…
CVE-2020-37268Medium· 6.3PoCPrint 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
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…