CVE-2026-72705: Rocq guard checker accepts fixpoint passed as higher-order argument (0 = 1 demonstrated)

Summary by Cyber Security News26 Oct 2026, 01:20 CET

About this summary. This is a short excerpt from the description that oss-security published with its article. Cyber Security News did not report or verify the underlying story. Read the original: https://seclists.org/oss-sec/2026/q4/383

Posted by Jonathan Brossard on Oct 25 1. Summary A soundness bug in the Rocq (formerly Coq) kernel's guard checker allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, tactics, plugins, or unsafe flags. Print Assumptions reports the proof as closed under the global context.

Read the full article at oss-security →

Source attribution: headline and facts are from oss-security (seclists.org). Summary method: excerpt of the source description. See our source attribution policy.

Related coverage

Node.js security release pre-alert

Open-source file sync tool rsync 3.5.2 fixes a CPU exhaustion flaw

Ghostunnel: Open-source TLS proxy with mutual authentication

Rails security releases: 8.0.5.2 and 8.1.4.1

Fixed Detectors, Moving Code: How Well Do Static Security Analyzers Hold Up over a Decade of C/C++ Evolution?

When Debate Amplifies Risk: Social-Bias Vulnerabilities in Multi-Agent Safety Deliberation