News · via oss-security
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…