Summary
Distinct module paths could become the same OCaml identifier during Rocq's native compilation, causing native computation to accept a false proof without additional axioms. The maintainers list versions 8.5 through 9.2.0 as affected and record this as a critical soundness bug. The naming fix was merged on September 7, 2026. The independent rocqchk checker rejects the reported false proof and is listed as unaffected by this bug.
Disclosure timeline
- Public disclosure
Credits
Reported by christos-cantina-security on behalf of Cantina.