That proof was artificially constructed specifically to show the exploit. It wasn't a real attempt at a proof that was later shown to be using an exploit.

I'm unaware of any serious proofs that have been shown to have a kernel exploit in them.