He once told me that he wasn't interested in formalizing his proof of Bloch-Kato, because he was sure it was right. (I should have asked him at the time how he could be so sure!)Oh this is interesting... do you remember when this conversation was happening? Because in these slides (https://www.math.ias.edu/vladimir/sites/math.ias.edu. ) he said "Next year I am starting a project of univalent formalization of my proof of Milnor’s Conjecture using this formalization of set theory as the starting point." (Page 11)vladimir/files/2014_09_ Bernays_3%20presentation.pdf