I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale

I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale. Eg. - Are you sure the compiler is correct? - Are you sure the OS is behaving correctly? - Are you sure the CPU isn't randomly glitching out? There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all. How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.