Description

Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.

Executive Summary

Technical Details

Mitigations

References

Additional Metadata

{
  "score": "6.3",
  "pubDate": "2026-08-24T20:16:40.560Z",
  "pubdate": "2026-08-24T20:16:40.560Z",
  "executiveSummary": "Coq contains an audit bypass vulnerability involving the Print Assumptions command and parameter inlining within module types.\nThe vulnerability type is an assumption tracking failure leading to soundness evasion, allowing arbitrary proposition proofs to be classified as closed under the global context.\nThe affected product is Coq, specifically recorded in dev/doc/critical-bugs.md as a non-fixed bug.\nThe risk is rated as moderate when the standalone checker coqchk is not utilized.\nAn attacker can exploit this behavior by leveraging universe inconsistency proofs within a module implementation and exposing them through an inlined parameter via functor application.\nExploitation bypasses the in-process audit provided by Print Assumptions, though the compiled file is successfully rejected by the standalone checker coqchk.",
  "technicalDetails": "The root cause of the vulnerability lies in the handling of universe checking states during parameter inlining in module types.\nWhen universe checking is disabled via Unset Universe Checking, terms are produced under this relaxed constraint.\nHowever, when a functor is applied, it inlines the body of the parameter and explicitly drops the internal record indicating that the term was originally built under Unset Universe Checking.\nConsequently, the resulting constant carries no trace of the unsafe operation, stripping away metadata that would normally flag the term as depending on inconsistent universes.\nThe attack flow proceeds as follows: first, a module implementation proves False by exploiting a universe inconsistency under disabled universe checking.\nSecond, this fraudulent proof is exposed through an inlined parameter within a module type.\nThird, when the Print Assumptions command is executed to verify the dependent proof, it fails to report that the definition was produced while universe checking was disabled.\nAs a result, Print Assumptions incorrectly reports the dependent proof as closed under the global context.\nThe vulnerable components involve the module system's parameter inlining mechanism and the Print Assumptions auditing routine.\nThis vulnerability requires local development manipulation where a user or developer constructs a proof using the affected module patterns.\nThe post-exploitation impact allows arbitrary propositions to pass internal in-process verification audits without raising warnings, although external validation via coqchk correctly identifies and rejects the compiled artifact."
}