Cyber ·
CVE-2026-72705: Rocq guard checker accepts a fixed point passed as higher-order argument, proving 0 = 1
A soundness flaw in the Rocq kernel guard checker lets a builder construct a verified proof of False, and of any proposition, without axioms, tactics, plugins or unsafe flags. The disclosure was posted to the oss-sec list on 25 October 2026.
Radar: the oss-sec list disclosed on 25 October 2026 the vulnerability CVE-2026-72705 in Rocq, a formal proof assistant. The kernel guard checker does not track recursive calls made through the arguments of a fixed point. As a result, a fixed point can pass itself as an argument and produce a proof of False and, by extension, of any proposition, including 0 = 1. According to the report, the proof uses no axioms, tactics, plugins or unsafe flags, and the Print Assumptions command shows it as closed in the global context. This means that the usual check does not detect the problem. This is an automatic translation summary of an original text; consult the full source for affected versions, fixes and technical details. Relevance for Rota Nacional: the platform does not fix or contain this flaw, which lies in formal verification software. Anyone using Rocq for proofs that support decisions should treat results as untrusted until the tool is updated.