Skip to content
Threat Feed
Subscribe

Tag

Formal-Verification

3 briefs RSS
medium advisory

Rocq Prover: Soundness vulnerability in guard checker (CVE-2026-72705)

A logic flaw in the Rocq kernel guard checker permits the construction of false proofs by failing to track recursive calls in fixpoints, undermining the integrity of formal verification.

Rocq Prover vulnerability formal-verification rocq
1c
high advisory

Lean 4: Kernel soundness vulnerability via nested inductive projections (CVE-2026-72844)

A soundness vulnerability in the Lean 4 kernel allows the construction of false mathematical proofs due to improper validation of structure projections and insufficient type-checking in the inductive definition process.

Lean 4 vulnerability formal-verification logic-soundness
1c
high advisory

Rocq: Soundness vulnerability in module system (CVE-2026-72714)

A logic soundness vulnerability in the Rocq kernel allows for the construction of invalid proofs due to improper state management of the universe checking flag after closing a module.

Rocq vulnerability formal-verification
1c