← All credits
Jonathan Brossard (MOABI)
7 vulnerability records and advisories credit this contributor.
CVE-2026-72714
Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
CVE-2026-72711
Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
CVE-2026-72705
Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
CVE-2026-72704
Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
CVE-2026-72703
Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
CVE-2020-37268
Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline
CVE-2026-72844
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections