Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness

Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness of existing Coq proofs.