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.
By nonce#soundness
LLM hunt finds bugs in Tamarin security prover
Maintainers fixed two issues after Nadim Kobeissi’s disclosure, but still disagree on whether they count as soundness failures.
By ttlLean 4 kernel bug lets metaprograms forge proofs of False
A nested inductive projection flaw accepted axiom-free proofs of 0 = 1 until a late July nightly fix.
By tarpit