#proof-assistants

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.