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#lean
Lean formalization of Julia Base surfaces hundreds of bugs
Miles Cranmer modeled concrete Base types and docstring promises as Lean theorems, filing 75 filtered reports after AI-assisted proof attempts failed.
By rvalue