CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated) — unfixed since 2020
// AI summary
Rocq/Coq has an unfixed soundness-audit bypass (CVE-2020-37268) allowing construction of a proof of False when Parameter Inline inlines the parameter body, omitting unsafe universe checking.
// from the source
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....