Executive brief
Rocq is an interactive theorem prover used to develop and verify formal mathematical proofs. A flaw in its Print Assumptions audit tool allows proofs that rely on unsafe universe-checking assumptions to be incorrectly reported as valid, potentially allowing false mathematical claims to pass internal verification checks. While the standalone coqchk validator catches this, teams relying only on Print Assumptions could deploy flawed proofs into production.
Technical details
The vulnerability is a logic error in how Rocq's Print Assumptions function reports proof dependencies when universe checking is disabled. When a definition is created with universe checking disabled and then inlined through a functor parameter, the inlining operation drops the record that the term was built unsafely, causing Print Assumptions to report the proof as closed under the global context even though it depends on an unsafe assumption. An attacker or careless developer can craft a module that proves False using a universe inconsistency, expose it through an inlined parameter, and have the dependency audit pass. The standalone coqchk checker correctly rejects such files, but projects relying solely on in-process Print Assumptions auditing can be affected. No patch availability is indicated in the advisory.
Affected products
- Rocq Rocq Prover
Timeline
- 2026-08-24: disclosed