None of the soundness bugs found in lean so far could have been plausibly exploited by accident. For example you might have to set up weird recursive types that never come up in ordinary mathematics. Of course, past performance is not indicative of future results.
