CVE-2026-72704 Detail
Received
This CVE record has recently been published to the CVE List and has been included within the NVD dataset. DescriptionThe guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged. Metrics
NVD enrichment efforts reference publicly available information to associate
vector strings. CVSS information contributed by other sources is also
displayed.
CVSS 4.0 Severity and Vector Strings:
CNA: VulnCheck
CVSS-B 6.8 MEDIUM
Vector: CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N
References to Advisories, Solutions, and ToolsBy selecting these links, you will be leaving NIST webspace. We have provided these links to other web sites because they may have information that would be of interest to you. No inferences should be drawn on account of other sites being referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the facts presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites. Please address comments about this page to [email protected].
Weakness Enumeration
Quick InfoCVE Dictionary Entry:CVE-2026-72704 NVD Published Date: 08/24/2026 NVD Last Modified: 08/24/2026 Source: VulnCheck |
|||||||||||||||||||||||||
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
Secure .gov websites use HTTPS
A lock (
) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.
Information Technology Laboratory
National Vulnerability Database
National Vulnerability Database
NVD
