rocq-cve-poc-22024
by Endrazine
Source repositories
CVEs (3)
| CVE | Vendor / Product | Sev | Risk | CVSS | EPSS | KEV | Published | Description |
|---|---|---|---|---|---|---|---|---|
| CVE-2026-72714 | Med | 0.41 | 6.3 | 0.00 | Aug 24, 2026 | 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… | ||
| CVE-2026-72704 | Med | 0.34 | 6.3 | 0.00 | Aug 24, 2026 | 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 recursive argument, which the guard… | ||
| CVE-2026-72703 | Med | 0.34 | 6.3 | 0.00 | Aug 24, 2026 | 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 calls, so when no body calls itself the… |
- risk 0.41cvss 6.3epss 0.00
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…
- risk 0.34cvss 6.3epss 0.00
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 recursive argument, which the guard…
- risk 0.34cvss 6.3epss 0.00
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 calls, so when no body calls itself the…