The time has come: Claude is able to poke holes in the dark corners of Rocq's kernel and come up with proofs of False!

The days of "our reasonable users use the unreasonable features only in reasonable ways so it's ok to have them" really are over. Can't wait until someone vibe codes a complicated proof without looking too closely at it (since it's been checked by the kernel, it must be fine!) only to later realise it was actually bogus and such a bug without the agent saying so...