CVE-2026-72703 (GCVE-0-2026-72703)
Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-09-24 14:18
VLAI
EPSS
VEX
Title
Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Summary
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Severity
6.3 (Medium)
SSVC
Exploitation: poc
Automatable: no
Technical Impact: partial
CISA Coordinator · CISA-ADP (v2.0.3)
Decision recorded 2026-08-27 14:12 UTC
CWE
- CWE-670 - Always-Incorrect Control Flow Implementation
Assigner
References
5 references
| URL | Tags |
|---|---|
| https://github.com/rocq-prover/rocq | product |
| https://github.com/rocq-prover/rocq/issues/21682 | issue-tracking |
| https://github.com/rocq-prover/rocq/pull/21684 | issue-trackingpatch |
| https://github.com/endrazine/rocq-cve-poc-21682 | exploit |
| https://www.vulncheck.com/advisories/rocq-prover-… | third-party-advisory |
Impacted products
1 product
| Vendor | Product | Version | CPE status | |
|---|---|---|---|---|
| rocq-prover | rocq |
Affected:
8.20 , < 9.2.0
(custom)
|
guessed |
Date Public
2026-02-28 00:00
{
"containers": {
"adp": [
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2026-72703",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2026-08-27T14:12:34.453Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
}
],
"cna": {
"affected": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"credits": [
{
"lang": "en",
"type": "finder",
"value": "Tristan St\u00e9rin"
},
{
"lang": "en",
"type": "finder",
"value": "Jonathan Brossard (MOABI)"
}
],
"datePublic": "2026-02-28T00:00:00.000Z",
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
}
],
"metrics": [
{
"cvssV4_0": {
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"privilegesRequired": "NONE",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"vectorString": "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",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH"
},
"format": "CVSS"
},
{
"cvssV3_1": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"format": "CVSS"
}
],
"problemTypes": [
{
"descriptions": [
{
"cweId": "CWE-670",
"description": "Always-Incorrect Control Flow Implementation",
"lang": "en",
"type": "CWE"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2026-09-24T14:18:50.897Z",
"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"shortName": "VulnCheck"
},
"references": [
{
"tags": [
"product"
],
"url": "https://github.com/rocq-prover/rocq"
},
{
"tags": [
"issue-tracking"
],
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"tags": [
"issue-tracking",
"patch"
],
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"tags": [
"exploit"
],
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"tags": [
"third-party-advisory"
],
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
}
],
"title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"x_generator": {
"engine": "vulncheck-endgame"
}
}
},
"cveMetadata": {
"assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"assignerShortName": "VulnCheck",
"cveId": "CVE-2026-72703",
"datePublished": "2026-08-24T20:08:30.607Z",
"dateReserved": "2026-08-10T13:02:20.829Z",
"dateUpdated": "2026-09-24T14:18:50.897Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.2",
"vulnerability-lookup:meta": {
"epss": {
"cve": "CVE-2026-72703",
"date": "2026-10-14",
"epss": "0.00176",
"percentile": "0.06653"
},
"nvd": {
"cve": {
"affected": [
{
"affectedData": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"source": "disclosure@vulncheck.com"
}
],
"cveTags": [],
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
},
{
"lang": "es",
"value": "El verificador de guardas en Rocq Prover trata un par\u00e1metro de un punto fijo mutuo anidado como uniforme sin examinar las llamadas entre los diferentes cuerpos de ese punto fijo. find_uniform_parameters en kernel/inductive.ml inspecciona solo las llamadas autorrecursivas, por lo que cuando ning\u00fan cuerpo se llama a s\u00ed mismo, la funci\u00f3n concluye que cada par\u00e1metro es uniforme. Un par\u00e1metro que crece a trav\u00e9s de una llamada cruzada de un cuerpo a otro, por lo tanto, mantiene la especificaci\u00f3n de subt\u00e9rmino que hered\u00f3 del punto fijo envolvente, y una llamada recursiva protegida por esa especificaci\u00f3n es aceptada aunque el argumento no sea estructuralmente menor. Una definici\u00f3n no terminante es admitida como estructuralmente decreciente, lo que produce un t\u00e9rmino cuyo valor es igual a su propio sucesor y, por lo tanto, una prueba de Falso, de la cual se deduce cualquier proposici\u00f3n. La prueba no requiere axiomas, plugins o banderas inseguras y Print Assumptions lo reporta como cerrado bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0."
}
],
"id": "CVE-2026-72703",
"lastModified": "2026-10-12T15:10:00.207",
"metrics": {
"cvssMetricV31": [
{
"cvssData": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"exploitabilityScore": 1.8,
"impactScore": 4.0,
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
],
"cvssMetricV40": [
{
"cvssData": {
"Automatable": "NOT_DEFINED",
"Recovery": "NOT_DEFINED",
"Safety": "NOT_DEFINED",
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"availabilityRequirement": "NOT_DEFINED",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"confidentialityRequirement": "NOT_DEFINED",
"exploitMaturity": "NOT_DEFINED",
"integrityRequirement": "NOT_DEFINED",
"modifiedAttackComplexity": "NOT_DEFINED",
"modifiedAttackRequirements": "NOT_DEFINED",
"modifiedAttackVector": "NOT_DEFINED",
"modifiedPrivilegesRequired": "NOT_DEFINED",
"modifiedSubAvailabilityImpact": "NOT_DEFINED",
"modifiedSubConfidentialityImpact": "NOT_DEFINED",
"modifiedSubIntegrityImpact": "NOT_DEFINED",
"modifiedUserInteraction": "NOT_DEFINED",
"modifiedVulnAvailabilityImpact": "NOT_DEFINED",
"modifiedVulnConfidentialityImpact": "NOT_DEFINED",
"modifiedVulnIntegrityImpact": "NOT_DEFINED",
"privilegesRequired": "NONE",
"providerUrgency": "NOT_DEFINED",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"valueDensity": "NOT_DEFINED",
"vectorString": "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/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH",
"vulnerabilityResponseEffort": "NOT_DEFINED"
},
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
],
"ssvcV203": [
{
"source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"ssvcData": {
"id": "CVE-2026-72703",
"options": [
{
"exploitation": "poc"
},
{
"automatable": "no"
},
{
"technicalImpact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
}
}
]
},
"published": "2026-08-24T20:17:18.240",
"references": [
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
}
],
"sourceIdentifier": "disclosure@vulncheck.com",
"vulnStatus": "Deferred",
"weaknesses": [
{
"description": [
{
"lang": "en",
"value": "CWE-670"
}
],
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
]
}
},
"redhat_vex": {
"current_release_date": "2026-08-24T21:18:43+00:00",
"cve": "CVE-2026-72703",
"id": "CVE-2026-72703",
"initial_release_date": "2026-08-24T20:08:30.607000+00:00",
"product_status:known_not_affected": "1",
"source": "Red Hat CSAF VEX",
"status": "final",
"title": "rocq: Rocq Prover: Logical Flaw Allows Arbitrary Proof Generation via Unchecked Cross-Calls",
"url": "https://security.access.redhat.com/data/csaf/v2/vex/2026/cve-2026-72703.json",
"version": "3"
},
"vulnrichment": {
"containers": {
"adp": [
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2026-72703",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2026-08-27T14:12:30.905Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
}
],
"cna": {
"affected": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"credits": [
{
"lang": "en",
"type": "finder",
"value": "Tristan St\u00e9rin"
},
{
"lang": "en",
"type": "finder",
"value": "Jonathan Brossard (MOABI)"
}
],
"datePublic": "2026-02-28T00:00:00.000Z",
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
}
],
"metrics": [
{
"cvssV4_0": {
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"privilegesRequired": "NONE",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"vectorString": "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",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH"
},
"format": "CVSS"
},
{
"cvssV3_1": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"format": "CVSS"
}
],
"problemTypes": [
{
"descriptions": [
{
"cweId": "CWE-670",
"description": "Always-Incorrect Control Flow Implementation",
"lang": "en",
"type": "CWE"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2026-09-24T14:18:50.897Z",
"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"shortName": "VulnCheck"
},
"references": [
{
"tags": [
"product"
],
"url": "https://github.com/rocq-prover/rocq"
},
{
"tags": [
"issue-tracking"
],
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"tags": [
"issue-tracking",
"patch"
],
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"tags": [
"exploit"
],
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"tags": [
"third-party-advisory"
],
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
}
],
"title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"x_generator": {
"engine": "vulncheck-endgame"
}
}
},
"cveMetadata": {
"assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"assignerShortName": "VulnCheck",
"cveId": "CVE-2026-72703",
"datePublished": "2026-08-24T20:08:30.607Z",
"dateReserved": "2026-08-10T13:02:20.829Z",
"dateUpdated": "2026-09-24T14:18:50.897Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.2"
}
}
}
Loading…
Loading…
Drag nodes to arrange them. Double-click a related vulnerability to open it, or a source to visit its link. The Physics button on the left tunes the layout and the simulation; the legend at the bottom left hides or shows nodes by kind and by sighting type.
Experimental. This forecast is provided for visualization only and may change without notice. Do not use it for operational decisions.
Forecast uses a logistic model when the trend is rising, or an exponential decay model when the trend is falling. Fitted via linearized least squares.
Sightings
| Author | Source | Type | Date | Other |
|---|
Nomenclature
- Seen: The vulnerability was mentioned, discussed, or observed by the user.
- Confirmed: The vulnerability has been validated from an analyst's perspective.
- Published Proof of Concept: A public proof of concept is available for this vulnerability.
- Exploited: The vulnerability was observed as exploited by the user who reported the sighting.
- Patched: The vulnerability was observed as successfully patched by the user who reported the sighting.
- Not exploited: The vulnerability was not observed as exploited by the user who reported the sighting.
- Not confirmed: The user expressed doubt about the validity of the vulnerability.
- Not patched: The vulnerability was not observed as successfully patched by the user who reported the sighting.
Vulnerability timeline
Sightings and recorded dates, grouped by day · UTC
Loading timeline…
Loading…
Loading…
The MITRE ATT&CK techniques below are AI-generated suggestions, inferred from the description of the
vulnerability by the CIRCL/vulnerability-attack-technique-classification-roberta-base
model, served locally by ML-Gateway.
They have not been verified by an analyst and are provided for guidance only.
The approach is described in our paper Mapping CVEs to MITRE ATT&CK Techniques: A Curated Gold-Set Classifier and the Limits of LLM-Assisted Label Expansion.
Browse all ATT&CK techniques and the vulnerabilities related to each.
The approach is described in our paper Mapping CVEs to MITRE ATT&CK Techniques: A Curated Gold-Set Classifier and the Limits of LLM-Assisted Label Expansion.
Browse all ATT&CK techniques and the vulnerabilities related to each.
Loading…
Related by attack behaviour
Vulnerabilities whose description is nearest to this one in the vector space of the CIRCL/vulnerability-attack-technique-biencoder model. This is a similarity search over the bi-encoder space (plain cosine), not a classification, and it has no measured accuracy.