One thing that wasn't always clear to me: how many of these examples crash due to bugs in the compiler/verifier, and how many because the type system is actually unsound?

Sometimes it is mentioned; a Rust example and a Java example were fixed years ago. So it seems... a little unfair? Obviously all software has bugs; compilers are no exception. Examples where the type system itself is unsound, and can't be fixed without a redesign, are IMO the only interesting ones.