rocq vulnerabilities
CVEs whose affected-version data names the rocq package. Each record lists the affected and patched versions; check a specific version with the dependency checker or POST /api/sbom.
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…