#rocq

Rocq and Lean 4 kernel bugs let checked proofs of False through

Four oss-security reports detail soundness and audit flaws that accept 0 = 1 without axioms, spanning two major proof assistants.