Voevodsky developed Univalent Foundations in order to catch subtle mistakes in his (and others) result:

"Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.

This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident."

More details on page 8 in the IAS newsletter article

https://www.ias.edu/sites/default/files/pdfs/publications/le...

There is also a Quanta article:

https://www.quantamagazine.org/univalent-foundations-redefin...