All bugs IDBugGuarantee brokenStatuslean-0001Kernel accepts wrong-structure projections, allowing an axiom-free proof of False kernel-soundness fixedlean-0002Kernel is_def_eq cache depended on the order of checks kernel-soundness fixedlean-0003String.Pos.Raw.extract: logical model and compiled code disagree compiler-soundness fixedlean-0004Kernel infer_let ignores dependencies in let-binding types—fixedlean-0005Substring comparison is not reflexive on malformed UTF-8—fixedlean-0006Kernel did not recognize sorts as Prop up to universe normalization kernel-soundness fixedlean-0007Declarations could use the kernel's _nested auxiliary type names kernel-soundness fixedlean-0008Kernel is_prop check did not require a sort kernel-soundness fixedlean-0009Reference count overflow corrupted runtime objects compiler-soundness fixedlean-0010Linux release builds linked GMP 6.1.2, which has an exploitable bug compiler-soundness fixedlean-0011Missing metavariable and free-variable checks in inductive.cpp—fixedlean-0012Universe parameters not checked in mutual definitions—fixedlean-0013Exported stubs of partial definitions were not marked unsafe—fixedlean-0014Kernel rejected a valid inductive predicate (universe normalization) kernel-completeness fixedlean-0015Kernel did not bound the size of Nat numerals it computes—fixed