Rocq-Prover

Exploited now

None of this vendor's CVEs are on CISA's known-exploited list.

Recent

• 6.3MediumAug 24, 2026Rocq-Prover rocqCVE-2026-72714Rocq 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 constrain
• 6.3MediumAug 24, 2026Rocq-Prover rocqCVE-2026-72705The 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 of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments
• 6.3MediumAug 24, 2026Rocq-Prover rocqCVE-2026-72704The 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 recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call
• 6.3MediumAug 24, 2026Rocq-Prover rocqCVE-2026-72703The 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 calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive c
• 6.3MediumAug 24, 2026Rocq-Prover rocqCVE-2020-37268Print 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 i

See every Rocq-Prover entry on the dashboard.

Top products

• rocq5 CVEs in the last year

Advisories

Official advisories from the last 90 days that name this vendor's CVEs.

• oss-security · Oct 26, 2026CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated) — unfixed since 2020CVE-2020-37268
• oss-security · Oct 26, 2026CVE-2026-72714: Rocq universe checking state desynchronised after module close (0 = 1 demonstrated) — 0-dayCVE-2026-72714
• oss-security · Oct 26, 2026CVE-2026-72705: Rocq guard checker accepts fixpoint passed as higher-order argument (0 = 1 demonstrated)CVE-2026-72705
• oss-security · Oct 26, 2026CVE-2026-72704: Rocq guard checker trusts corrupted recursive tree after transport (0 = 1 demonstrated) — 0-dayCVE-2026-72704
• oss-security · Oct 26, 2026CVE-2026-72703: Rocq guard checker accepts non-terminating fixpoint via unchecked cross-calls (0 = 1 demonstrated)CVE-2026-72703