CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated) — unfixed since 2020

Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness-audit bypass in the Rocq (formerly Coq) module system allows construction of a proof of False that Print Assumptions reports as closed under the global context — no axioms, no unsafe flags visible. When a module type declares Parameter Inline and functor application inlines the parameter's body, the metadata recording that the original definition was produced under Unset Universe Checking is dropped....

Published 26-Oct-2026 01:00 UTC · First seen 26-Oct-2026 00:58 UTC

Sources

• Open Source Security · 26-Oct-2026