...[ More ]

Coq versions 8.11 through 8.20 and Rocq Prover versions through 9.2.0 contain a proof auditing vulnerability involving the Parameter Inline mechanism in module functors. Definitions created with universe checking disabled can be inlined without preserving the unsafe universe checking metadata,...