Skip to content
Fedora 45 Rocq Critical Integrity Bypass and Logic Flaws 2026

Fedora 45 Rocq Critical Integrity Bypass and Logic Flaws 2026

Linuxsecurity •LinuxSecurity Advisories • October 6, 2026

Running self-managed GitLab? Critical flaws could allow server code execution. Check the fixes. ×

Rocq is a formal proof management system. It provides a formal language to

write mathematical definitions, executable algorithms and theorems together

with an environment for semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of programming

languages (e.g., the CompCert compiler certification project, or the Bedrock

verified low-level programming library), the formalization of mathematics

(e.g., the full formalization of the Feit-Thompson theorem or homotopy type

theory) and teaching.

This is a mass rebuild of the OCaml ecosystem with OCaml 5.5.1, which fixes two security bugs. See for details. In addition, rocq has been updated to version 9.3.0, which also fixes several CVEs. New upstream development version 1.61.4 New upstream development version 2.13.7

* Sun Sep 27 2026 Jerry James - 9.3.0-2 - Disable native compilation for aarch64 * Sun Sep 27 2026 Jerry James - 9.3.0-1 - Version 9.3.0 - Drop upstreamed dune patch * Tue Sep 15 2026 Richard W.M. Jones - 9.2.0-4 - OCaml 5.5.1 rebuild

* Sun Sep 27 2026 Jerry James - 9.3.0-2 - Disable native compilation for aarch64 * Sun Sep 27 2026 Jerry James - 9.3.0-1 - Version 9.3.0 - Drop upstreamed dune patch * Tue Sep 15 2026 Richard W.M. Jones - 9.2.0-4 - OCaml 5.5.1 rebuild

[ 1 ] Bug #2443780 - CVE-2026-28364 ocaml: OCaml: Remote code execution via buffer over-read in Marshal deserialization [fedora-all] [ 2 ] Bug #2520289 - rocq-stdlib-9.2.0 is available [ 3 ] Bug #2523138 - CVE-2020-37268 rocq: Coq and Rocq Provers: Logical inconsistency bypass via Print Assumptions omission [fedora-all] [ 4 ] Bug #2523145 - CVE-2026-72703 rocq: Rocq Prover: Logical Flaw Allows Arbitrary Proof Generation via Unchecked Cross-Calls [fedora-all] [ 5 ] Bug #2523146 - CVE-2026-72705 rocq: Rocq Prover: Logical inconsistency via untracked higher-order fixpoint arguments [fedora-all] [ 6 ] Bug #2523147 - CVE-2026-72714 rocq: Rocq Prover: Critical integrity by...

This update can be installed with the "dnf" update program. Use su -c 'dnf upgrade --advisory FEDORA-2026-403bcf6fd8' at the command line. For more information, refer to the dnf documentation available at

Get the latest News and Insights

Get the latest Linux and open source security news straight to your inbox.

Linux Security - Your source for Top Linux News, Advisories, HOWTOs and Feature Releases