Print Assumptions fails to flag that a definition was built while universe checking was disabled when that definition is later exposed through an inlined parameter in a module type. A module that proves False using a universe inconsistency can therefore be brought into the caller’s context and reported as a closed proof by Print Assumptions. This allows an attacker to construct an apparently valid proof of an arbitrary proposition while the underlying reasoning is unsound. The bug does not affect the compiled file directly – the standalone checker coqchk rejects the output – but it undermines internal audit mechanisms that rely on Print Assumptions.

The vulnerability affects the Rocq Prover (rocq-prover:rocq). No specific product versions were listed, so the issue applies to any version of Rocq that contains the described code path.

The CVSS score of 6.8 indicates moderate severity. EPSS data is unavailable and the bug is not listed in the CISA KEV catalog, suggesting it is not a widely exploited vulnerability. The most likely attack vector is a local user with the ability to construct Rocq modules that disable universe checking and then inline them, or a build system that relies on Print Assumptions to confirm proof integrity. Because the compiled file is flagged by coqchk, the risk is mitigated when that tool is used, but if a project relies solely on Print Assumptions for certification, the vulnerability could allow undetected false proofs to be accepted.